FSM file format

From MCRL2

Introduction

This page describes the FSM file format for storing labelled transition systems (LTS). Files in this format are accepted as input by several LTS visualisation tools in the mCRL2 toolset as well as several tools made by Hannes Pretorius and FSMView. FSM files usually have the extension '.fsm'.

Description

An FSM file is a human-readable, plain-text file that specifies an LTS. Its contents are of the following form:

PARAMETERS
'---'
STATES
'---'
TRANSITIONS

containing three sections:

• The first section specifies the state parameters and their domains;
• The second section specifies the states of the LTS;
• The third section specifies the transitions of the LTS.

These sections are separated by lines that contain three dashes: ---.

The format of each of these sections is described separately below.

Parameters section

The parameters section defines the state parameters (or state variables) and their domains of possible values. In every state of the LTS, each of the parameters has one specific value from its domain.

At least one parameter should be specified. Every parameter is specified on a separate line of the following form:

PARAMETER_NAME '(' DOMAIN_CARDINALITY ')' DOMAIN_NAME ('"'DOMAIN_VALUE'"')*

containing the following items:

• The parameter name: a string of alphanumerical characters;
• The domain cardinality: a natural number;
• The domain name: a string of alphanumerical characters;
• A list of domain values: a space-separated list of quoted values, where every value is a string of characters that does not contain quotes (").

The number of domain values should be equal to the domain cardinality. If the domain cardinality is 0, then the parameter will be ignored. It will not be visible in the tool and the corresponding state values in the states section are ignored.

States section

The states section defines the number of states and the value of every parameter in every state.

At least one state should be specified. The first state specified is taken to be the initial state of the LTS. Every state is specified on a separate line of the following form:

(PARAMETER_VALUE)*

being a list of parameter values: a space-separated list of natural numbers.

The number of parameter values should be equal to the number of parameters defined in the parameters section, including parameters with a domain cardinality of 0.

The ith value in the list specifies the value of the ith parameter of the parameters section in the following way: a value of n specifies that in this state, that parameter has the nth value from its domain. These values are 0-based, meaning that a value of 0 corresponds to the first domain value of that parameter.

Every value should be at least 0 and smaller than the domain cardinality of the corresponding parameter. If that domain cardinality is 0, then the latter restriction does not apply and the value will be ignored.

Transitions section

The transitions section defines the transitions between the states of the LTS.

Every transition is specified on a separate line of the following form:

SOURCE_STATE TARGET_STATE '"'LABEL'"'

containing the following items:

• The source state: a positive natural number;
• The target state: a positive natural number;
• The label: a quoted string of characters that does not contain quotes (").

A value of n for either of the states indicates the nth state of the states section. Each of these values should be at least 1 and at most the number of states specified in the states section.

Example

The following FSM file specifies the LTS depicted in the figure above. The state parameter values are indicated next to every state. The state identifiers used in the transitions section of the FSM file are shown inside every state.

b(2) Bool "F" "T"
n(2) Nat "1" "2"
---
0 0
0 1
1 0
1 1
---
1 2 "increase"
1 3 "on"
2 4 "on"
2 1 "decrease"
3 1 "off"
3 4 "increase"
4 2 "off"
4 3 "decrease"