main

all

Syntax: all domain do statement;

It executes a statement on each element from a given domain (domain can be a set of instances of a given module or any defined enumerated type).

Example:

  type ip_colour=(red, green, blue);

  trans
    when system.failure_indication
      priority highest
	    to closed
		  begin
		    all net: network do
			all color:ip_colour do
			  begin
			    detach net.p[colour];
			  end;
			terminate net;
		  end;

any

Syntax 1: any domain do (where domain is a list of local variables)

It executes a transition for all elements from a given set.

Example:

  trans
    from S1 to S2
      any n:1..2; k:3..4 do
        when p[n].m
        begin
          variable:=k;
        end;
		
  { is equal to }
  
  trans
    from S1 to S2
	   when p[1].m
	   begin
	     variable:=3;
	   end;
  trans
    from S1 to S2
	   when p[2].m
	   begin
	     variable:=3;
	   end;
  trans
    from S1 to S2
	   when p[1].m
	   begin
	     variable:=4;
	   end;
  trans
    from S1 to S2
	   when p[2].m
	   begin
	     variable:=4;
	   end;

Syntax 2: variable = any Type

Declaration of a variable, that has any value of a given type.

Example:

MaxRetrans = any Integer

attach

Syntax: attach external-ip to child-external-ip

It links an external parent interaction point to an external child interaction point. As the result, interactions from a queue, associated with a parent ip, would go to directly to a queue associated with an ip of child.

Example:

  attach A.p1 to B.p2; { where A and B are modules with ips: p1 and p2}

begin, end

See trans.

channel

Syntax: channel CHANNEL_ID(role1, role2);
    by role1: interaction11; .. interaction1N;
    by role2: interaction21; .. interaction2N;
    by role1, role2: interaction31; .. interaction3N;

In Estelle all modules communicate through channels. Each of those channels is defined by names of modules, that it connects, and a set of messages (interactions), that can go through it. A link between a channel and a module is an interaction point.

Example:

  channel communication( sender, receiver )
    by sender: Send_date;
    by receiver: Send_ack;

connect

Syntax: connect connect-ip1 to connect-ip2;

It links:

internal interaction point of module with external interaction point of its child;
internal interaction points of a given module;

Modules cannot manage connections of theirs interaction points.

delay

Syntax 1: delay( time ); ( time is an integer )

Suspends an execution for a given interval (unit of time is defined for a whole specification by keyword timescale). A delay clause may be associated only with a spontaneous transitions.

Syntax 2: delay( time1, time2 ); ( time1, time2 are integers )

Suspends an execution of transition for at least time1 period and at most time2 period of time. A delay clause may be associated only with a spontaneous transitions.

exist

Syntax: exist domain suchthat Boolean_expression;

It checks if exists an instance of a given module, that fulfils a condition (defined by a Boolean_expression).

Example:

  specification for_test SYSTEMPROCESS;
  INITIALIZE
    BEGIN
      IF exist a:65..75; b:char
        SUCHTHAT (ord(a)=ord(b))
          THEN { WRITELN('YES') }	
       ELSE { WRITELN('NO') }	
    END;
   END.

for

Syntax: for i:=initial_value to | downto final_value
do statement;

A statement is executed once for each value from a range initial_value to final_value.

Example:

  specification for_test SYSTEMPROCESS;
  TRANS
    VAR i:INTEGER;
      BEGIN
	    FOR i:=1 TO 10 DO
		   { WRITE(i) }	
        END;
      END.

forone

Syntax: forone domain
    suchthat Boolean_expression
    do statement1
    otherwise statement2

It executes a statement1 on each instance (from a given domain), that fulfils a Boolean_expression and a statement2 on each instance (from a given domain), that does not fulfil it.

Example:

  SPECIFICATION test_forone_1 SYSTEMPROCESS;

  PROCEDURE junk;
  BEGIN
    FORONE x:1..10 SUCHTHAT ord(x)*ord(x)>10
      DO { WRITELN(x,' * ',x,' > 10') }		
    FORONE x:1..10 SUCHTHAT ord(x)*ord(x)>100
      DO { WRITELN(x,' * ',x,' > 100') }	
  END;

  INITIALIZE
    BEGIN
      junk;
    END;
  END.

from

Syntax: from state1 to state2

An expression is used to define a transition. It defines a state, that module must be in, in order to fire a transition.

See trans.

function

Syntax: function identifier [(parameter_list)] : result_type
procedure_block;

A definition of a function.

if

Syntax: if Boolean_expression then statement1
else statement2

Specify a condition (Boolean_expression), under which a statement1 may be executed. Otherwise it executes statement2.

init

Syntax: init module_variable with body_identifier
[actual_module_parameter_list]

It creates a new instance of a given module.

Example:

  init A with BodyForModuleA;
  { or } 
  init A with BodyForModuleA( 1 ); { execution with parameters }

initizalize

Syntax: initialize

It begins inicialisation part of a module body or of a whole system.

Example:

  modvar
    DaemonInstance : Daemon;
	GameInstance : Game;
	PlayerInstance : Player;
  initialize
    begin
	  init DaemonInstance with DaemonBody;
	  init GameInstance with GameBody;
	  init PlayerInstance with PlayerBody;
	  connect PlayerInstance.G to GameInstance.P;  { G, P, D - are interaction points of given modules }
      connect DaemonBody.D to GameInstance.D
    end;

ip, queue

Syntax: ip ip_id: channel_id( role );

Each module can have many inputs and outputs, called interaction points. There exist two types of such points: internal (defined in module body) and external ones (defined in module header). With each of them is associated a channel, that links it with interaction point of the same or other module (to link interaction points keywords connect and attach are used).
An interaction point has, associated with it, an unbounded FIFO queue, where are kept messages incoming from other interaction points. This queue can belong only to one ip point (individual queue) or can be common to all ip of a given module (common queue).
A parameter role determines, with which end of channel a given interaction point is associated.

Example:

  channel C1 (r1,r2);
           by r1:          
               event1;     { <-- interactions go through C1 channel to module r1 }
           by r2:
               event5;     { <-- interactions go through C1 channel to module r2 }

  module P1_M process;
    ip P1_IP: C1(r1) individual queue; { <-- declaration of interaction point }
  end;

module process: activity:

Definition of a module in Estelle has two parts: definition of a module header and definition of a module body. In a module header, there should be such information as type of module (systemprocess, systemactivity, process, activity), definition of exported variables, parameters and (external) interaction points of a given module. Definition of a module body begins with keyword body, after which follows name of the module header, name of the module body and definition of a body or keyword external.
A module can have more than one body.

Example:

  module A systemactivity( R:boolean )
    ip p1: channel1( role2 );
       p2: channel2( role1 );
    export X,Y: integer;
  end;

  body C for A; external;
  { or }
  body C for A; { body definition } end;

modvar

Syntax: modvar name : header_identifier;

It is used to declare instances of modules. Those instances may be created statically or dynamically. See init, terminate and release.

output

Syntax: output ip_reference.interaction_identifier
output ip_reference.interaction_identifier( actual_parameter_list )

It is used to send a message through a given interaction point. A message can have parameters.

Example:

output p1.REQUEST( 3, true );

primitive

Body of a function may be written not in Estelle but in other language (for example in C). Function described as external is not defined in Estelle specification, but somewhere outside of it.

Example:

  procedure Push( value: ValueType; var stack: StackType);
  primitive;

  procedure Pop( value: ValueType; var stack: StackType);
  primitive;

priority

Syntax: priority priority_constant ( where priority_constant is a positive integer )

It sets priority of a transition.

Example:

  trans
    from IDLE to AK_SENT
	  priority 1
	    begin
	      ...
	    end;

procedure

Sytax: procedure identifier [(parameter_list)]
procedure_block;

Definition of a procedure.

provided

Syntax: provided (Boolean_expression | "otherwise" )

Specifies a condition (Boolean_expression), under which transition will be executed.

Example:

  trans
    from IDLE to AK_SENT
	  provided ( ack_no > 0 ) and ( ack_no < 10 )
	    begin
	      ...
	    end;

release

Syntax: release module_variable;

It kills a module and unbinds all its interaction points (in opposite to terminate, which destroys them, causing any interaction in their queues to be lost). So, execution of release X, where X is a body of a module that gives this commend, is equal to:

Execution in any order disconnect X and detach X;
Killing an instance of the module X and all its children;

Result of release operation is the same as execution of sequence deattach X (or/and disconnect X) and terminate X. A module can kill its children and theirs offspring, but not itself or any other module (that is not its offspring).

same

If a state after a transition is defined as same, it means that as automata after a transition does not change its state. It is useful, when a given transition, can be executed from a set of states.

Example:

  stateset EITHER=[EVEN, ODD];
  ...
  from EITHER to same
    begin
	  ...
	end

  { is equal to }

  from EVEN to EVEN
    begin
	  ...
	end

  from ODD to ODD
    begin
	  ...
	end

specification

Syntax: specification Spec_name [system_class];
    [default_option]
    [time_option]
      body_definition
    end.

Definition of a main module, which parts of are all other modules.
A specification has following attributes:

system_class - can be systemprocess or systemactivity. See trans.
default_option - a type of queue that is assumed for a whole system. It can be an individual queue or a common queue. See ip.
time_scale - unit of time for the system. See timescale.

Example:

specification MySpec;
  default individual queue;
  timescale seconds;

  ... { definition of internal modules headers and bodies, definitions of channels and
initialisation part of a whole system }

end.

state

Syntax: state identifier_list;

Behaviour of a module is described by is states and transitions between them. To define states of a module a keyword state is used.

Example:

state: IDLE, WAIT, OPEN, CLOSED

stateset

Syntax: stateset identifier = [identifier_list]

It defines a set of states, e.g. a set of error states can be subscribed as ERROR.

Example:

stateset IDWA = [IDLE, WAIT]

suchthat

See exist, forone.

terminate

Syntax: terminate module_variable;

In opposite to release, is does not unbind interaction points, but destroys them, causing all messages in their queues to be lost. A module can kill its children and theirs offspring, but not itself or any other module (that is not its offspring).

timescale

Syntax: timescale identifier; ( where identifier can have following values: hours, minutes, seconds, milliseconds, microseconds ).

It sets unit of time for a whole specification.

to

Syntax: from state1 to state2

It describes a state (or stateset), in which a module can be after a transition. See trans

trans

Syntax: trans
clause_group
transition_block

A transition has two parts. The first one, called clause group, can include following expressions:

when - describes an interaction point and a message, that has to be at a head of a queue associated with this interaction point, in order a transition takes place.
from - describes a state (or stateset) of module before a transition;
to - describes a state (or stateset) of module after a transition;
provided - describes a condition, that must be fulfilled, in order a transition takes place.
priority - describes a priority associated with a transition;
delay - describes a delay of transition execution;

Second part of transition, called transition block, is a sequence of Pascal and Estelle expressions, enclosed between keywords begin and end.

Example:

  trans
    from IDLE
	  priority medium
	    when N.DATA_INDICATION
		  name t1: begin
			output U.DATA_INDICATION
			ak_no:=ak_no+1
		  end;

when

Syntax: when ip_reference.interaction;

It defines an interaction point and a message that has to be at a head of a queue associated with this interaction point, in order a transition takes place.

Example:

  trans
    when P.Probe
	  from EVEN to ODD
	    begin
		  ...
		end;

while

Syntax: while Boolean_expression do statement;

A loop - a statement is repeatedly executed, until a value of a Boolean_expression is 0.

Example:

  while i>0 do
    begin
      i:=i div 2;
      x:=sqtr(x)
    end

with

Syntax 1: with record_variable_list do statement;

Execution of a statement on a set of records.

Example:

  with date do
    if month = 12 then 
      begin
        month:=1; year:=year+1
      end
    else mounth:=mount+1

{ is equal to }

  if date.month = 12 then
     begin date.month:=1; date.year+1
	 end
  else date.month:=date.month+1

Syntax 2: init module_header with body_for_module;

Creation of a module. See init.