User manual/chi2mcrl2

From MCRL2

User manual

Tool manual pages chi2mcrl2 diagraphica formcheck grapemcrl2 lps2lts lps2pbes lps2torx lpsactionrename lpsbinary lpsbisim2pbes lpsconfcheck lpsconstelm lpsinfo lpsinvelm lpsparelm lpsparunfold lpspp lpsrealelm lpsrewr lpssim lpssumelm lpssuminst lpsuntime lpsxsim lts2lps ltscompare ltsconvert ltsgraph ltsinfo ltsmin ltsview lysa2mcrl2 mcrl22lps mcrl2-gui mcrl2i pbesinst pbes2bool pbesconstelm pbesinfo pbesparelm pbespareqelm pbespgsolve pbespp pbesrewr pnml2mcrl2 squadt tbf2lps tracepp txt2lps txt2pbes

Contents

Convert a Chi specification to a matching mCRL2 process specification.

Contents 1 Synopsis 2 Short description 3 Options 4 Detailed description 4.1 Supported Language Features 4.1.1 Variable Classes 4.1.2 Constant definitions 4.1.3 Imports 4.1.4 Enumerations 4.1.5 Functions 4.1.6 Processes 4.1.7 Data types 5 Author 6 Reporting bugs

Synopsis

chi2mcrl2 [OPTION]... [INFILE [OUTFILE]]

Short description

chi2mcrl2 translates a Chi specification to a matching mCRL2 specification. For all the supported Chi operators individual translations to mCRL2 summands (with their associated data parameters) are constructed.

Currently, only non-timed/non-hybrid Chi specifications can be translated. If a specification is timed, e.g. the Chi statement delay, the time progress is translated to a "skip". If hybrid statements are used, e.g. the Chi Statement cont , the translation will fail to translate.

Options

OPTION can be any of the following:

-n, --no-state

no state parameters are generated when translating Chi processes

Standard options:

-q, --quiet

do not display warnings

-v, --verbose

display concise intermediate messages

-d, --debug

display detailed intermediate messages

-h, --help

display help message

--version

display version information

Detailed description

Supported Language Features

Like mCRL2, Chi also has a variety of tools for different translation and simulation purposes. Due to this variety it is hard to keep track of all the supported language features. We give an overview of the supported language features by chi2mcrl2, similar to the Chi Tools page. Note that the presented link shows a "Chi to μCRL translation", which is the predecessor of mCRL2.

In the tables below, a “+” means that the feature is supported and a “-” means that the language is not supported.

Variable Classes

Each variable in a Chi program belongs to a variable class. Below are the supported variable classes for chi2mcrl2.

Variable Class	chi2mcrl2
cont vardecl	-
alg vardecl	-
var vardecl	+
alg parameter	-
alg parameter	-

with the following footnotes:

• vardecl means “variable declaration”
• parameter means “parameter declarations” (in headers of models, processes)

Constant definitions

Constant definitions are not supported by chi2mcrl2.

Imports

Imports are a general concept in Chi. Library files can be imported but also other Chi specifications or even libraries written in other languages are considered useful. However the import feature is not supported in chi2mcrl2.

Enumerations

Enumeration definitions are not supported by chi2mcrl2.

Functions

Enumeration definitions are not supported by chi2mcrl2.

Processes

The following language features are supported.

Feature	chi2mcrl2
time in guards	-
folding	-
alternative composition	+
parallel composition	#1
process instantiation	#1
recdef instantiation	-
deadlock	+
inconsistent	-
delay predicate	-
action predicate	#2
any delay	-
signal emission	-
delay operator	#3
jump enable	-
local variable scope	-
local channel scope	-
local recdef scope	-
recdef	-
urgent communication	-
encapsulation	-
guard	+

with the following footnotes:

• recdef means “recursion definition” in the above table.
• #1: parallel composition is allowed only in a model definition
• #2: instead skips and multi-assignments are translated
• #3: delay is translated to a silent action

Data types

In the table below are the supported data types for chi2mcrl2.

Data type	chi2mcrl2
booleans	+
naturals	+
reals	-
lists	+
sets	+
dictionaries	-
vectors	-
records	+
distributions	-
matrices	-

Author

Written by Frank Stappers.

Reporting bugs

Report bugs at our issue tracking system.

---

Tool manual pages

diagraphica