SAL to CDL Translation

Advanced User Guide

Author: Tamim Nassar
Last updated: 1/5/2005

In this document:

Overview
Translation constraints
Module translation
Variable declaration
Definitions
Initialization
Type declaration
Transitions
Conditional expression
Non-deterministic assignment

Overview

Translation from SAL to CDL is not trivial. When attempting to translate models from SAL to CDL we may face many problems that need special techniques to solve. This document will show these problems and how we can solve them,

Translation constraints

Although most translation problems can be solved, there are some that are too difficult to solve. Here is a list of translation constraints that the translator must enforce:

Function declarations and complex type declarations cannot be translated.
Explicit declaration is required in all type declarations including arrays.
- Array [1..N] OF INTEGER is allowed if N a constant.
- Array [x:INTEGER | x<N] is not allowed.

Module translation

The non-combinational SAL module looks like this:

name: MODULE =

BEGIN

	INPUT/OUTPUT/GLOBAL/LOCAL	(variable declarations)

	DEFINITION			(definitions)

	INITIALIZATION			(initialization)

	TRANSITION			(transitions)

END;

When translating the module to the Core representation, we have to know how each part will be represented. Although definitions and transitions are trivial, the variable definitions and the initializations are not as trivial.

The core representation should look like this

Module name(input,output and global variables){

	VAR local variables (initialized)

	DEFINE definitions

	TRANS transitions

}

The translation of each one of these parts will be shown below.

Combinational SAL module translation is trivial. Here's an example:

Sal	Core
system: MODULE = (USER \|\| USER);	MODULE system() { (( USER() \|\| USER() )) }

Variable declaration

Variable declaration is intuitive.

Sal

Core

Q: MODULE =

  BEGIN

    INPUT in : INTEGER

    OUTPUT out : INTEGER

    LOCAL arr : ARRAY NATURAL OF Data

    GLOBAL glob : NATURAL

  END;

MODULE Q(in:INTEGER, out:INTEGER, glob:INTEGER){ 

    VAR arr: ARRAY [MAX_SIZE] of Data

}

Definitions

Definitions translation is intuitive.

Sal	Core
DEFINITION first = contents[head]	DEFINE first := contents[head];

Initialization

When a local variable is initialized, the translation should have INITVAL set in the variable definition. However, when an input variable or a global variable is initialized, an initialization transformation must be added to the module.

Sal

Core

clock: MODULE = 
BEGIN
   INPUT time_out: TIMEOUT_ARRAY
   OUTPUT time: TIME
   INITIALIZATION
      time = 0
   TRANSITION
      [ time_elapses: 
	time < time_out -->
		 time' = time_out ]
END;

MODULE clock(
	time_out: ARRAY [ MAX_SIZE ] OF TIME ,
	time	: TIME )
{ 
   VAR 
      inited: boolean INITVAL false ;

   Trans T#init:
      enable: inited := false;
      assign: inited := true ; time := 0 ; 

   Trans T#3:
      enable: inited /\ ( time < time_out ) ;
      assign: time ' := time_out ; 
}

Another example of initialization is when the element is initialized to a set of values:

Sal

Core

process: MODULE =
BEGIN
   INPUT time: TIME
   GLOBAL lock: LOCK_VALUE
   OUTPUT timeout: TIME
   LOCAL pc: PC
   INITIALIZATION
      pc = sleeping;
      timeout IN { x: TIME | time < x };
      lock = 0
   TRANSITION
   [ waking_up: 
      pc = sleeping AND 
	time = timeout AND lock = 0 
		--> pc' = waiting;
      timeout' IN { x: TIME |
		 time < x AND x <= time + delta1 } 

   [] try_again_later:
       pc = sleeping AND time = timeout AND lock /= 0 
	-->
       timeout' IN { x: TIME | time < x }
   ]
END;

MODULE process(
	time: TIME, 
	lock: LOCK_VALUE, 
	timeout: TIME)
{
   VAR
      pc: PC INITVAL sleeping;
      inited: boolean INITVAL false;
      x: TIME;

   Trans T#init: 
      enable: inited := false;
      assign: inited:= true; lock: = 0;
      relation: (timeout' = x) /\ (time < x);

   Trans T#2: 
      enable: inited /\ (((pc = sleeping) /\ 
                  (time = timeout)) /\ (lock = 0));
      assign: pc':= waiting;
      relation: (timeout' = x) /\ ((time < x) /\ 
                  (x < = (time+delta1)));

   Trans T#3: 
      enable: inited /\ (((pc = sleeping) /\ 
                  (time = timeout)) /\ (lock! = 0));
      relation: (timeout' = x) /\ (time < x);
}

Type Declaration

The basic types can easily be translated. NATURAL, INTEGER and NZINTEGER will be translated as Integer; BOOLEAN will stay the same and although CDL does not support REAL but we can translate it into Integer.
We have to remember that in CDL types can only be defined as atomic types or sub-sets and cannot be defined as arrays.
Tuples and Records don't exist in CDL. Therefore their elements will be split as follows

Sal	Core
Queue: TYPE = [# data: INTEGER, tl: BOOLEAN #];	TYPE T#Queue#data: INTEGER; T#Queue#tl: BOOLEAN;

Complex type declarations such as tuples/records inside tuples/records or arrays inside arrays are not supported.

Transitions

There are two types of transitions:

Transitions with guarded commands
Transitions with assignments only

The first type of transitions is easy to translate:

Sal

Core

ENTERING_AND_SEMAPHOR_IS_FALSE:(label of trans.)

  (user_state = entering)

           AND (semaphore = false) -->

     user_state' = critical;

     semaphore' = true

Trans T#2: (some label)

  enable: ( user_state = entering )

              /\ ( semaphore = false );

  assign: user_state':= critical;

          semaphore' := true;

The second type is not as trivial as we can see in the following example

Sal	Core
TRANSITION head' = a tail' = b	Trans T#2: (some label) enable: true; relation: (head'=a)/\(tail'=b)

The reason we used the relation here is to make a common ground for the conditions and the assignments as we will next see:

Conditional expressions

There is no need to split the transition into several transitions each with a unique enable condition. We can translate the transition by creating a logical combination of all the assignments in the conditions. This technique will work also for conditions inside conditions.

Sal

Core

TRANSITION

  head' = 

     IF op = pop THEN head+1 ELSE head ENDIF;

  tail' = 

     IF op = push THEN tail+1 ELSE tail ENDIF

Trans T#2: (some label)

  enable: true;

  relation: 

      (((op=pop) /\ (head'=(head+1))

           \/ (!(op=pop) /\ (head'=head)))

      /\ 

      (((op=push) /\ (tail'=(tail+1))

           \/ (!(op=push) /\ (tail'=tail)))

Note that an other possible translation for conditional expressions is where each condition is put into a separate transformation. However, to implement this translation we have to check all the conditions and if there are conditions that are equivalent then they should be in the same transition. Also, if there are two conditions, then we need to generate four transitions to cover all the possibilities, and if we have three conditions then we will need to create 8 transitions. Therefore, this translation option is very problematic.

Non-deterministic assignment

Some non-deterministic assignment problems are trivial:

Sal	Core
TRANSITION NON_DETERMINISTIC_IDLE_OR_ENTERING: user_state = idle --> user_state' IN {idle, entering}	Trans T#2: (some label) enable: user_state = idle ; assign: user_state' := {entering, idle};

Other non-deterministic assgnment problems are more complicated. The solution is adding relations.

Sal

Core

process: MODULE =
BEGIN
   INPUT time: TIME
   GLOBAL lock: LOCK_VALUE
   OUTPUT timeout: TIME
   LOCAL pc: PC
   INITIALIZATION
      pc = sleeping;
      timeout IN { x: TIME | time < x };
      lock = 0
   TRANSITION
   [ waking_up: 
      pc = sleeping AND 
	time = timeout AND lock = 0 --> 
      pc' = waiting;
      timeout' IN { x: TIME | 
		time < x AND x <= time + delta1 } 

   [] try_again_later:
      pc = sleeping AND
	 time = timeout AND lock /= 0 -->
      timeout' IN { x: TIME | time < x }
   ]
END;

MODULE process(
	time: TIME, 
	lock: LOCK_VALUE,
	timeout: TIME){
   VAR
      pc: PC INITVAL sleeping;
      inited: boolean INITVAL false;
      x: TIME;

   Trans T#init: 
      enable: inited := false;
      assign: inited:= true; lock: = 0;
      relation: (timeout' = x) /\ (time < x);

   Trans T#2: 
      enable: inited /\ (((pc = sleeping) /\ 
                  (time = timeout)) /\ (lock = 0));
      assign: pc':= waiting;
      relation: (timeout' = x) /\ ((time < x) /\ 
                  (x < = (time+delta1)));

   Trans T#3: 
      enable: inited /\ (((pc = sleeping) /\ 
                  (time = timeout)) /\ (lock! = 0));
      relation: (timeout' = x) /\ (time < x);
}