MoDeST Language Manual

Ric Klaren

Formal Methods and Tools Group, University of Twente
      
      

Table of Contents
Preface
Colophon
1. Introduction
Short Introduction to Process Algebra's
2. MoDeST Language Constructs
Basic Language Constructs
Sequential composition
ALT statement
DO Statement
PALT statement
GUARD statements
Data
Functions
User defined types
The Not-So-Basic Language Constructs
Process Definitions
PAR statement - Parallel composition
Exceptions
3. MoDeST Language Grammar
Preliminaries
MoDeST Descriptions
defaults
description
Declarations
variable_declaration
modifier
qualified_type
identifier_or_array_decl
range
action_decl
Examples
Functions and Processes
process_definition
param_definition
parameter
function_definition
process_body
parameterized_object
arguments
Examples
Type definitions
type_definition
Examples
'Simple' statements
local_process
assignment
assignment_op
perform_action
assignment_block
assignments
Examples
Action Labels and friends
label_expr
label_modification
labels
labels_by_labels
Examples
Program control
sequential_processes
alt_stmnt
loop_stmnt
alternative
palt_stmnt
weight
guarded_process
parallel_composition
try_block
Expressions
expression
simple_expression
additive_expr
or_expr
and_expr
bitor_expr
bitexclor_expr
bitand_expr
equality_expr
relational_expr
shift_expr
multiplicative_expr
unary_expr
base_expr
qualified_identifier
indexing
Sets
A. GNU Free Documentation License
PREAMBLE
APPLICABILITY AND DEFINITIONS
VERBATIM COPYING
COPYING IN QUANTITY
MODIFICATIONS
COMBINING DOCUMENTS
COLLECTIONS OF DOCUMENTS
AGGREGATION WITH INDEPENDENT WORKS
TRANSLATION
TERMINATION
FUTURE REVISIONS OF THIS LICENSE
ADDENDUM: How to use this License for your documents
List of Tables
2-1. MoDeST Builtin Types
2-2. MoDeST Operators
2-3. MoDeST Builtin Distributions
List of Figures
2-1. Transition in a Stochastic Automaton
List of Examples
2-1. A very simple MoDeST program.
2-2. A simple MoDeST program with two processes.
2-3. A simple MoDeST program with two processes.
  Next
  Preface