Sismic user manual¶

https://travis-ci.org/AlexandreDecan/sismic.svg?branch=master

https://coveralls.io/repos/AlexandreDecan/sismic/badge.svg?branch=master&service=github

https://api.codacy.com/project/badge/grade/10d0a71b01c144859db571ddf17bb7d4

https://readthedocs.org/projects/sismic/badge/?version=master

About¶

Statecharts are a well-known visual modeling language for specifying the executable behavior of reactive event-based systems. The essential complexity of statechart models solicits the need for advanced model testing and validation techniques. Sismic is a statechart library for Python (version 3.5 or higher) providing a set of tools to define, validate, simulate, execute and test statecharts. Sismic is a recursive acronym that stands for Sismic Interactive Statechart Model Interpreter and Checker.

Sismic is mainly developed by Dr. Alexandre Decan as part of his research activities at the Software Engineering Lab of the University of Mons. Sismic is released as open source under the GNU Lesser General Public Licence version 3.0 (LGPLv3).

The scientific article A method for testing and validating executable statechart models, published in 2018 in the Springer Software & Systems Modeling journal, describes the method and techniques for modeling, testing and validating statecharts, as supported by Sismic.

Features¶

Sismic provides the following features:

An easy way to define and to import statecharts, based on the human-friendly YAML markup language
A statechart interpreter offering a discrete, step-by-step, and fully observable simulation engine
Fully controllable simulation clock, with support for real and simulated time
Built-in support for expressing actions and guards using regular Python code, can be easily extended to other programming languages
A design-by-contract approach for statecharts: contracts can be specified to express invariants, pre- and postconditions on states and transitions
Runtime checking of behavioral properties expressed as statecharts
Built-in support for behavior-driven development
Support for communication between statecharts
Synchronous and asynchronous executions
Statechart visualization using PlantUML

The semantics of the statechart interpreter is based on the specification of the SCXML semantics (with a few exceptions), but can be easily tuned to other semantics. Sismic statecharts provides full support for the majority of the UML 2 statechart concepts:

simple states, composite states, orthogonal (parallel) states, initial and final states, shallow and deep history states
state transitions, guarded transitions, automatic (eventless) transitions, internal transitions and transition priorities
statechart variables and their initialisation
state entry and exit actions, transition actions
internal and external events, parametrized events, delayed events

Installation¶

Using pip¶

Sismic requires Python >=3.5, and can be installed using pip as usual: pip install sismic. This will install the latest stable version. Starting from release 1.0.0, Sismic adheres to a semantic versioning scheme.

You can isolate Sismic installation by using virtual environments:

Get the tool to create virtual environments: pip install virtualenv
Create the environment: virtualenv -p python3.5 env
Jump into: source env/bin/activate
Install Sismic: pip install sismic

Consider using pew or pipenv to manage your virtual environments.

The development version can also be installed directly from its git repository: pip install git+git://github.com/AlexandreDecan/sismic.git

From GitHub¶

You can also install Sismic from its repository by cloning it.

Get the tool to create virtual environments: pip install virtualenv
Create the environment: virtualenv -p python3.5 env
Jump into: source env/bin/activate
Clone the repository: git clone https://github.com/AlexandreDecan/sismic
Install Sismic: pip install . or pip install -e . (editable mode)
Install test dependencies: pip install -r requirements.txt

Sismic is now available from the root directory. Its code is in the sismic directory. The documentation can be built from the docs directory using make html.

Tests are available both for the code and the documentation:

make doctest in the docs directory (documentation tests)
python -m pytest tests/ from the root directory (code tests)

Statecharts definition¶

About statecharts¶

Statecharts are a well-known visual language for modeling the executable behavior of complex reactive event-based systems. They were invented in the 1980s by David Harel, and have gained a more widespread adoption since they became part of the UML modeling standard.

Statecharts offer more sophisticated modeling concepts than the more classical state diagrams of finite state machines. For example, they support hierarchical composition of states, orthogonal regions to express parallel execution, guarded transitions, and actions on transitions or states. Different flavours of executable semantics for statecharts have been proposed in the literature and in existing tools.

Defining statecharts in YAML¶

Because Sismic is supposed to be independent of a particular visual modeling tool, and easy to integrate in other programs without requiring the implementation of a visual notation, statecharts are expressed using YAML, a human-friendly textual notation (the alternative of using something like SCXML was discarded because its notation is too verbose and not really “human-readable”).

This section explains how the elements that compose a valid statechart in Sismic can be defined using YAML. If you are not familiar with YAML, have a look at YAML official documentation.

See also

While statecharts can be defined in YAML, they can be defined in pure Python too. Moreover, Statechart instances exhibit several methods to query and manipulate statecharts (e.g.: rename_state(), rotate_transition(), copy_from_statechart(), etc.). Consider looking at Statechart API for more information.

See also

Experimental import/export support for AMOLA specifications of statecharts is available as an extension of Sismic. AMOLA is notably used in ASEME IDE, which can be used to graphically create, edit and visualize statecharts. More information on Extensions for Sismic.

Statechart¶

The root of the YAML file must declare a statechart:

statechart:
  name: Name of the statechart
  description: Description of the statechart
  root state:
    [...]

The name and the root state keys are mandatory, the description is optional. The root state key contains a state definition (see below). If specific code needs to be executed during initialization of the statechart, this can be specified using preamble. In this example, the code is written in Python.

statechart:
  name: statechart containing initialization code
  preamble: x = 1

Code can be written on multiple lines as follows:

preamble: |
  x = 1
  y = 2

States¶

A statechart must declare a root state. Each state consist of at least a mandatory name. Depending on the state type, other optional fields can be declared.

statechart:
  name: statechart with defined state
  root state:
    name: root

Entry and exit actions¶

For each declared state, the optional on entry and on exit fields can be used to specify the code that has to be executed when entering and leaving the state:

- name: s1
  on entry: x += 1
  on exit: |
    x -= 1
    y = 2

Final states¶

A final state can be declared by specifying type: final:

- name: s1
  type: final

Shallow and deep history states¶

History states can be declared as follows:

type: shallow history to declare a shallow history state;
type: deep history to declare a deep history state.

- name: history state
  type: shallow history

A history state can optionally declare a default initial memory using memory. Importantly, the memory value must refer to a parent’s substate.

- name: history state
  type: deep history
  memory: s1

Composite states¶

A state that is neither a final state nor a history state can contain nested states. Such a state is commonly called a composite state.

- name: composite state
  states:
    - name: nested state 1
    - name: nested state 2
      states:
        - name: nested state 2a

A composite state can define its initial state using initial.

- name: composite state
  initial: nested state 1
  states:
    - name: nested state 1
    - name: nested state 2
      initial: nested state a2
      states:
        - name: nested state 2a

Note

Unlike UML, but similarly to SCXML, Sismic does not explicitly represent the concept of region. A region is essentially a logical set of nested states, and thus can be viewed as a specialization of a composite state.

Orthogonal states¶

Orthogonal states (sometimes referred as parallel states) allow to specify multiple nested statecharts running in parallel. They must declare their nested states using parallel states instead of states.

statechart:
  name: statechart containing multiple orthogonal states
  root state:
    name: processes
    parallel states:
      - name: process 1
      - name: process 2

Transitions¶

Transitions between states, compound states and parallel states can be declared with the transitions field. Transitions typically specify a target state using the target field:

- name: state with transitions
  transitions:
    - target: other state

Other optional fields can be specified for a transition: a guard (a Boolean expression that will be evaluated to determine if the transition can be followed), an event (name of the event that will trigger the transition), an action (code that will be executed if the transition is processed). Here is a full example of a transition specification:

- name: state with an outgoing transition
  transitions:
    - target: some other state
      event: click
      guard: x > 1
      action: print('Hello World!')

One type of transition, called an internal transition, does not require to declare a target. Instead, it must either define an event or define a guard to determine when it should become active (otherwise, infinite loops would occur during simulation or execution).

Notice that such a transition does not trigger the on entry and on exit of its state, and can thus be used to model an internal action.

Priorities can be set for transitions using the priority property. By default, all transitions have a priority of 0. A priority can be any integer, or low (equivalent to -1) or high (equivalent to 1).

Note

Transition priorities are considered after the default semantics of Sismic, i.e., after the eventless transition first and inner-first/source state semantics. Because of this, transition priorities cannot be used to, e.g., give priority to a transition with event versus a transition without event.

Statechart examples¶

Elevator¶

The Elevator statechart is one of the running examples in this documentation. Its visual description generated from Sismic using PlantUML looks as follows:

The corresponding YAML description is given below.

statechart:
  name: Elevator
  preamble: |
    current = 0
    destination = 0
    doors_open = True
  root state:
    name: active
    parallel states:
      - name: movingElevator
        initial: doorsOpen
        states:
          - name: doorsOpen
            transitions:
              - target: doorsClosed
                guard: destination != current
                action: doors_open = False
              - target: doorsClosed
                guard: after(10) and current > 0
                action: |
                  destination = 0
                  doors_open = False
          - name: doorsClosed
            transitions:
              - target: movingUp
                guard: destination > current
              - target: movingDown
                guard: destination < current and destination >= 0
          - name: moving
            transitions:
              - target: doorsOpen
                guard: destination == current
                action: doors_open = True
            states:
              - name: movingUp
                on entry: current = current + 1
                transitions:
                  - target: movingUp
                    guard: destination > current
              - name: movingDown
                on entry: current = current - 1
                transitions:
                  - target: movingDown
                    guard: destination < current
      - name: floorListener
        initial: floorSelecting
        states:
          - name: floorSelecting
            transitions:
              - target: floorSelecting
                event: floorSelected
                action: destination = event.floor

Other examples¶

Some other examples can be found in the Git repository of the project, in docs/examples.

Importing and validating statecharts¶

The Statechart class provides several methods to construct, to query and to manipulate a statechart. A YAML definition of a statechart can be easily imported to a Statechart instance. The module sismic.io provides a convenient loader import_from_yaml() which takes a textual YAML definition of a statechart and returns a Statechart instance.

sismic.io.import_from_yaml(text=None, filepath=None, *, ignore_schema=False, ignore_validation=False)

Import a statechart from a YAML representation (first argument) or a YAML file (filepath argument).

Unless specified, the structure contained in the YAML is validated against a predefined schema (see sismic.io.SCHEMA), and the resulting statechart is validated using its validate() method.

Parameters:	text (`Optional`[`str`]) – A YAML text. If not provided, filepath argument has to be provided. filepath (`Optional`[`str`]) – A path to a YAML file. ignore_schema (`bool`) – set to True to disable yaml validation. ignore_validation (`bool`) – set to True to disable statechart validation.
Return type:	`Statechart`
Returns:	a Statechart instance

For example:

from sismic.io import import_from_yaml
from sismic.model import Statechart

with open('examples/elevator/elevator.yaml') as f:
    statechart = import_from_yaml(f)
    assert isinstance(statechart, Statechart)

The function also supports importing from a given filepath:

statechart = import_from_yaml(filepath='examples/elevator/elevator.yaml')
assert isinstance(statechart, Statechart)

The parser performs several checks using Statechart’s validate method. It also does an automatic validation against some kind of schema to prevent erroneous keys. See schema library for more information about the semantics.

class SCHEMA:
    contract = {schema.Or('before', 'after', 'always'): schema.Use(str)}

    transition = {
        schema.Optional('target'): schema.Use(str),
        schema.Optional('event'): schema.Use(str),
        schema.Optional('guard'): schema.Use(str),
        schema.Optional('action'): schema.Use(str),
        schema.Optional('contract'): [contract],
        schema.Optional('priority'): schema.Or(schema.Use(int), 'high', 'low'),
    }

    state = dict()  # type: ignore
    state.update({
        'name': schema.Use(str),
        schema.Optional('type'): schema.Or('final', 'shallow history', 'deep history'),
        schema.Optional('on entry'): schema.Use(str),
        schema.Optional('on exit'): schema.Use(str),
        schema.Optional('transitions'): [transition],
        schema.Optional('contract'): [contract],
        schema.Optional('initial'): schema.Use(str),
        schema.Optional('parallel states'): [state],
        schema.Optional('states'): [state],
    })

    statechart = {
        'statechart': {
            'name': schema.Use(str),
            schema.Optional('description'): schema.Use(str),
            schema.Optional('preamble'): schema.Use(str),
            'root state': state,
        }
    }

Visualising statecharts¶

Sismic is not bundle with any graphical tool that can be used to edit or even view a statechart. Module sismic.io contains routines that can be used to (import and) export statecharts to other formats, some of them being used by third-party tools that support visualising (or editing) statecharts.

Notably, module sismic.io contains a function export_to_plantuml() that exports a given statechart to PlantUML, a tool based on graphviz that can automatically render statecharts (to some extent). An online version of PlantUML can be found here.

For example, the elevator statechart can be exported to the following PlantUML file, which in turns can be used to generate the previously given representation of the elevator.

@startuml
title Elevator
state "active" as active {
  state "floorListener" as floorListener {
    [*] -right-> floorSelecting
    state "floorSelecting" as floorSelecting {
      floorSelecting --> floorSelecting : floorSelected / destination = event.floor
    }
  }
  --
  state "movingElevator" as movingElevator {
    [*] -right-> doorsOpen
    state "moving" as moving {
      moving --> doorsOpen : [destination == current] / doors_open = True
      state "movingDown" as movingDown {
        movingDown : **entry** / current = current - 1
        movingDown --> movingDown : [destination < current]
      }
      state "movingUp" as movingUp {
        movingUp : **entry** / current = current + 1
        movingUp --> movingUp : [destination > current]
      }
    }
    state "doorsClosed" as doorsClosed {
      doorsClosed --> movingUp : [destination > current]
      doorsClosed --> movingDown : [destination < current and destination >= 0]
    }
    state "doorsOpen" as doorsOpen {
      doorsOpen -right-> doorsClosed : [destination != current] / doors_open = False
      doorsOpen -right-> doorsClosed : [after(10) and current > 0] / destination = 0; doors_open = False
    }
  }
}
@enduml

See also

PlantUML’s rendering can be modified to some extent by adjusting the notation used for transitions. By default, --> transitions correspond to downward transitions of good length.

A transition can be shortened by using -> instead of -->, and the direction of a transition can be changed by using -up->, -right->, -down-> or -left->. Both changes can be applied at the same time using -u->, -r->, -d-> or -l->. See PlantUML documentation for more information.

If you already exported a statechart to PlantUML and made some changes to the direction or length of the transitions, it is likely that you want to keep these changes when exporting again the (possibly modified) statechart to PlantUML.

The export_to_plantuml() function accepts two optional (mutually exclusive) parameters based_on and based_on_filepath that can be used to provide an earlier version of a PlantUML text representation (or a path to such a version if based_on_filepath is used). This will then be used to incorporate as much as possible the changes made on transitions.

sismic.io.export_to_plantuml(statechart, filepath=None, *, based_on=None, based_on_filepath=None, statechart_name=True, statechart_description=False, statechart_preamble=False, state_contracts=False, state_action=True, transition_contracts=False, transition_action=True)

Export given statechart to plantUML (see http://plantuml/plantuml). If a filepath is provided, also save the output to this file.

Due to the way statecharts are representing, and due to the presence of features that are specific to Sismic, the resulting statechart representation does not include all the informations. For example, final states and history states won’t have name, actions and contracts.

If a previously exported representation for the statechart is provided, either as text (based_on parameter) or as a filepath (based_on_filepath parameter), it will attempt to reuse the modifications made to the transitions (their direction and length).

Parameters:	statechart (`Statechart`) – statechart to export filepath (`Optional`[`str`]) – save output to given filepath, if provided based_on (`Optional`[`str`]) – existing representation of the statechart in PlantUML based_on_filepath (`Optional`[`str`]) – filepath to an existing representation of the statechart in PlantUML statechart_name (`bool`) – include the name of the statechart statechart_description (`bool`) – include the description of the statechart statechart_preamble (`bool`) – include the preamble of the statechart state_contracts (`bool`) – include state contracts state_action (`bool`) – include state actions (on entry, on exit and internal transitions) transition_contracts (`bool`) – include transition contracts transition_action (`bool`) – include actions on transition
Return type:	`str`
Returns:	textual representation using plantuml

Statecharts visualization¶

Sismic is not bundle with any graphical tool that can be used to edit or even view a statechart. Module sismic.io contains routines that can be used to (import and) export statecharts to other formats, some of them being used by third-party tools that support visualising (or editing) statecharts.

Notably, module sismic.io contains a function export_to_plantuml() that exports a given statechart to PlantUML, a tool based on graphviz that can automatically render statecharts (to some extent). An online version of PlantUML can be found here.

Function export_to_plantuml() can be directly called from the command-line without having to run a Python interpreter, through the sismic-plantuml (or python -m sismic.io.plantuml) command-line interface.

usage: sismic-plantuml [-h] [--based-on based] [--show-description]
                    [--show-preamble] [--show-state-contracts]
                    [--show-transition-contracts] [--hide-state-action]
                    [--hide-name] [--hide-transition-action]
                    statechart

Command-line utility to export Sismic statecharts to plantUML.
See sismic.io.export_to_plantuml for more informations.

positional arguments:
statechart                      A YAML file describing a statechart

optional arguments:
-h, --help                      show this help message and exit
--based-on based                A previously exported PlantUML representation
                                    for this statechart
--show-description              Show statechart description
--show-preamble                 Show statechart preamble
--show-state-contracts          Show state contracts
--show-transition-contracts     Show transition contracts
--hide-state-action             Hide state action
--hide-name                     Hide statechart name
--hide-transition-action        Hide transition action

For example, the elevator statechart presented in the previous section can be exported to the following PlantUML excerpt.

@startuml
title Elevator
state "active" as active {
  state "floorListener" as floorListener {
    [*] -right-> floorSelecting
    state "floorSelecting" as floorSelecting {
      floorSelecting --> floorSelecting : floorSelected / destination = event.floor
    }
  }
  --
  state "movingElevator" as movingElevator {
    [*] -right-> doorsOpen
    state "moving" as moving {
      moving --> doorsOpen : [destination == current] / doors_open = True
      state "movingDown" as movingDown {
        movingDown : **entry** / current = current - 1
        movingDown --> movingDown : [destination < current]
      }
      state "movingUp" as movingUp {
        movingUp : **entry** / current = current + 1
        movingUp --> movingUp : [destination > current]
      }
    }
    state "doorsClosed" as doorsClosed {
      doorsClosed --> movingUp : [destination > current]
      doorsClosed --> movingDown : [destination < current and destination >= 0]
    }
    state "doorsOpen" as doorsOpen {
      doorsOpen -right-> doorsClosed : [destination != current] / doors_open = False
      doorsOpen -right-> doorsClosed : [after(10) and current > 0] / destination = 0; doors_open = False
    }
  }
}
@enduml

This PlantUML description can automatically be converted to the following statechart representation using the PlantUML tool (an online version can be found here).