ScenarioTools SML Implementation

This wiki contains information about the implementation of the Eclipse plugins constituting the ScenarioTools IDE. On this page you can find an overview of the project's components.

SML Metamodel and Editor

Scenario Modeling Language

SML Runtime

SML Runtime

IDE plugins

Synthesis & Realizability Checking

A specification can be checked for realizability by trying to synthesize a controller that does not violate it. If that is not possible, a counter-example can be generated. The algorithm used for synthesis utilizes the SML runtime.

Simulation

Given an object system, SML specifications can be simulated in the IDE. The simulation plugin utilizes the Eclipse debug framework and the SML runtime.

Statespace Exploration

For small systems it may be desirable to view the complete statespace of a specification/object system pair. The state space exploration plugin explores the complete state space of the specification and outputs the resulting graph.

Builder

The builder plugin is used for updating files derived from specification and runtime models. Builder

wiki clone URL

$ git clone https://jgreenyer@bitbucket.org/jgreenyer/scenariotools-sml.git/wiki