MCRL2 LTS file format

From MCRL2

Introduction

This page describes the mCRL2 file format for storing labelled transition systems (LTSs). The usual extension of these files is '.lts'.

Description

An mCRL2 LTS file consist of two sections (although the second section is optional). The first section, starting at offset 0, is an SVC file with type mCRL2 or mCRL2+info. The appendix +info indicates whether states are stored as just numbers or as actual mCRL2 states. The actions of transitions are always stored as a pair of an mCRL2 multiaction and an mCRL2 expression of sort Time. The latter may also be Nil in absence of timing. The precise form of states and transitions is as follows. Note that we use the notation and non-terminals form the mCRL2 internal format description.

<State>            ::= STATE(<DataExpr>, ...,<DataExpr>)

<TransitionAction> ::= pair(<MultAct>,<DataExprOrNil>)

Optionally, this SVC file is followed by a second section containing information such as a data specification or state parameter names. This section consist of an ATerm in Binary format followed by a 64-bit offset (little endian) and a marker '   1STL2LRCm' (note the three initial spaces). The offset indicates where this section starts in the file. The ATerm is of the following form.

<mCRL2LTS1>      ::= mCRL2LTS1(<DataSpecOrNil>,<ParamSpecOrNil>,<ActSpecOrNil>)

<DataSpecOrNil>  ::= <DataSpec>
                   | Nil

<ParamSpecOrNil> ::= ParamSpec(<DataVarId>*)
                   | Nil

<ActSpecOrNil>   ::= <ActSpec>
                   | Nil