We’re here to help you

Menu

Checking Well-formedness

Well-formedness Checks

The syntax as defined in [[Syntax and Semantics]] defines a language which is not restrictive enough for practical use. This page describes a collection of well-formedness checks that are defined on top of the syntax. Some of these checks are "common sense", other ones are needed to define appropriate semantics.

The well-formedness checks in alphabetical order:

Action value discarded: enable
Actions are not allowed here
ActionStatement only allowed within OnEventStatement
AssignmentStatement only allowed within OnEventStatement

Binding directions do not match
Binding two wildcards is not allowed
BlockingStatement not allowed in interface behaviour
BlockingStatement not allowed with multiple provides ports
BlockingStatement not allowed within other BlockingStatement

Component is part of a cyclic binding
Component with behaviour must have at least one provides port: Alarm
Component with behaviour needs at least one trigger event: Alarm
Constant expression expected: c

Enum type name must not be equal to model name: NameClash
Event is not a valid trigger: console.detected
Event is not an action: console.arm
External port must be bound to external port: r2

Function calls are not allowed here
Function does not return a value in all cases
Function value discarded: negate

Illegal is not allowed in functions
Illegal is not allowed in if-then-else statements
Illegal must be the only Statement in a compound
Injected Port has out event: i
Inout Parameter is not allowed for out Event
Interface must define at least one event: Sensor
Interface must define behaviour: Sensor

OnEventStatement not allowed within other OnEventStatement
Only declarative Statement allowed here
Only imperative Statement allowed here
Otherwise guard combined with non GuardedStatement is not allowed
Otherwise guard combined with second otherwise is not allowed
Out Event with non void return type is not allowed: evt
Out Parameter is not allowed for out Event

Parameter Binding not allowed here
Parameter type must be a data type: Code
Port name must not be equal to model name: NameClash
Port is bound twice: alarm.console
Port is not bound: alarm.console
Port is not bound: console

Reply not allowed on 'requires' Port: 'sensor'
Return Statement not allowed here

Statement violates tail recursion in recursive Function
System composition is recursive

Variable name must not be equal to model name: NameClash

Wildcard can be bound to a provided port only

The various types of well-formedness checks:

  • Well-formedness checks that avoid name clashes in models.

  • Top level well-formedness checks, which check state restrictions on the occurrence of events in interfaces and components.

  • Well-formedness checks on the Behaviour part of a model come, which can be grouped in a number of categories:

    • Initialization: The initialization of state variables is restricted.

    • Directional: triggers and actions are expected at different places.

    • Nesting: the imperative part of the language (AssignmentStatements, ActionStatements,FunctionCallStatements) are only allowed in the 'leaves' of the language constructs.

    • Mixing: The mix of Statements within a CompoundStatements is restricted.

    • Guards: There are some restrictions on what is allowed in a Guard.

    • Functions: a function body should be imperative, and have a well-defined return.

      a trigger is an event prefixed by 'on' in the behaviour, an action is an event inside the body of a trigger.
  • Well-formedness checks for a composite Component:

    • Binding: all ports should be bound correctly.

Well-formedness Checks — Name clashes

The type system of Dezyne restricts the naming of new types and variables in such a way that all occurrences of these names can be uniquely coupled to their introduction.

On top of these rules some extra restrictions are posed. Without these restrictions code generation for languages such as C++ becomes cumbersome.

Enum type name must not be equal to model name: NameClash

When in the context of an interface an enumeration type is declared, its name must be different from that interface’s name. An example:

 1  interface NameClash {
 2    enum NameClash { E1, E2 };
 3    in void e();
 4    behaviour {
 5      on e: {}
 6    }
 7  }

This results in the following error message:

2:8: Well-formedness error: Enum type name must not be equal to model name: I1

This restriction also holds for enumeration types declared in a model (either component or interface) behaviour. An example:

 1  component NameClash {
 2    provides I1 p;
 3    behaviour {
 4      enum NameClash { E1, E2 };
 5      on p.e(): {}
 6    }
 7  }

This results in the following error message:

4:10: Well-formedness error: Enum type name must not be equal to model name: 'NameClash'

Port name must not be equal to model name: NameClash

When in a component a port is declared, its name must be different from that component’s name. An example:

 1  component NameClash {
 2    provides I1 NameClash;
 3    behaviour {
 4      on NameClash.e(): {}
 5    }
 6  }

This results in the following error message:

2:15: Well-formedness error: Port name must not be equal to model name: 'NameClash'

Variable name must not be equal to model name: NameClash

When in a model (either component or interface) behaviour a state variable is declared, its name must be different from that model’s name. An example:

 1  component NameClash {
 2    provides I1 p;
 3    behaviour {
 4      bool NameClash = false;
 5      on p.e(): {}
 6    }
 7  }

This results in the following error message:

4:10: Well-formedness error: Variable name must not be equal to model name: 'NameClash'

Well-formedness Checks — Top level

Interface must define behaviour: Sensor

Interfaces without behaviour are not allowed. No adequate default behaviour is available:

 1  interface Sensor {
 2    in void enable();
 3    in void disable();
 4    out void triggered();
 5    out void disabled();
 6  }

This results in the following error message:

1:11: Interface must define behaviour: Sensor

Interface must define at least one event: Sensor

Completely 'passive' interfaces are not allowed; at least one in or out event is required:

 1  interface Sensor {
 2    behaviour {
 3      // ...
 4    }
 5  }

This results in the following error message:

1:11: Interface must define at least one event: Sensor

Out Event with non void return type is not allowed: evt

Only in Event can have a return type.

 1  interface Sensor {
 2    enum Value{ New, Old };
 3    in void enable();
 4    in void disable();
 5    out Value triggered();
 6    out void disabled();
 7    ...
 8  }

This results in the following error message:

5:13: Out Event with non void return type is not allowed: triggered

Component with behaviour needs at least one trigger event: Alarm

Any Component with a behaviour specification is supposed to be 'reactive'. This implies that it should have at least one provides Interface with an in Event, or at least one requires Interface with an out Event. Such an Event acts as a 'trigger' for the Component to react on. So-called 'active' Components are not allowed (yet) in the Dezyne language.

An example:

  1  interface Sensor {
  2    in void activate();
  3    in void deactivate();
  4    behaviour { ... }
  5  }
  6
  7  component Alarm {
  8    requires Sensor sensor;
  9    behaviour { ... }
 10  }

Another example:

  1  interface Siren {
  2    out void start();
  3    out void stop();
  4    behaviour { ... }
  5  }
  6
  7  component Alarm {
  8    provides Siren siren;
  9    behaviour { ... }
 10  }

Both examples result in the following error message:

7:11: Component with behaviour needs at least one trigger event: Alarm

Component with behaviour must have at least one provides port: Alarm

Any Component with a behaviour specification must have a provides port through which the Component is activated. An example:

 1  component Alarm {
 2    requires Sensor sensor;
 3    behaviour { ... }
 4  }

The examples result in the following error message:

1:11: Component with behaviour must have at least one provides port: Alarm

Well-formedness Checks — Initialization

Constant expression expected: c

In the initialization of state variables only 'constant expressions' are allowed. This means no variables may occur in the initialization expression. An example:

  1   behaviour {
  2     enum E { E1, E2 };
  3     E s = E.E1;
  4
  5     bool b = c;
  6     bool c = true;
  7     bool d = true && c;
  8     bool e = true && false;
  9     bool g = s.E1;
 10     ...
 11   }

This results in the following error messages:

5:14: Well-formedness error: Constant expression expected: 'c'
7:22: Well-formedness error: Constant expression expected: 'c'
9:14: Well-formedness error: Constant expression expected: 's'

Well-formedness Checks — Directional

Event is not an action: console.arm

Event console.arm is used as action, but is introduced as a trigger.

In an InterfaceModel this indicates the Event is defined as an in event.

In a DesignModel this indicates that either it is an in Event of a provides interface of the design, or an out Event of a requires interface.

Event is not a valid trigger: console.detected

Event console.detected is used as trigger, but is introduced as an action.

In an InterfaceModel this indicates the Event is defined as an out event.

In a DesignModel this indicates that either it is an out Event of a provides interface of the design, or an in Event of a requires interface.

Well-formedness Checks — Nesting

The nesting of language constructs is restricted. When we conceptually 'expand' CompoundStatements, two Statement levels can be identified:

  • The outer level we call declarative. It consists of exactly one OnEventStatement, optionally guarded at either side with GuardedStatements and at most one BlockingStatement. Valid examples are:

 1  on sensor.triggered(): { ... }
 2  [guard1] [guard2] on sensor.triggered(): { ... }
 3  [guard1] on sensor.triggered(): [guard2] { ... }
 4  on sensor.triggered(): [guard1] [guard2] { ... }
 5  [guard1] blocking [guard2] on sensor.triggered(): { ... }
 6  blocking [guard1] on sensor.triggered(): [guard2] { ... }
 7  on sensor.triggered(): [guard1] [guard2] blocking { ... }
  • The inner level we call imperative. It consists of ActionStatements and AssignmentStatements. Imperative statements are only allowed within a declarative context:

 1  [state.Armed]
 2  {
 3    on sensor.triggered():
 4    {
 5      // the imperative part:
 6      console.detected();
 7      state = States.Triggered;
 8    }
 9  }

AssignmentStatement only allowed within OnEventStatement

An AssignmentStatement occurred outside the scope of a declarative context:

 1  [state.Armed]
 2  {
 3    state = States.Triggered;
 4  }

This results in the following error message:

3:3: Well-formedness error: AssignmentStatement only allowed within OnEventStatement

ActionStatement only allowed within OnEventStatement

An ActionStatement occurred outside the scope of a declarative context:

 1  [state.Disarming]
 2  {
 3    console.detected();
 4  }

This results in the following error message:

3:3: Well-formedness error: ActionStatement only allowed within OnEventStatement

OnEventStatement not allowed within other OnEventStatement

A second OnEventStatement occurred in the declarative context:

 1  on console.arm():
 2  {
 3    [state.Disarming]
 4    {
 5      on sensor.triggered():
 6      { ... }
 7    }
 8  }

This results in the following error message:

5:5: Well-formedness error: OnEventStatement not allowed within other OnEventStatement

BlockingStatement not allowed within other BlockingStatement

A second BlockingStatement occurred in the declarative context:

 1  blocking on console.arm():
 2  {
 3    [state.Disarming]
 4    {
 5      blocking
 6      { ... }
 7    }
 8  }

This results in the following error message:

5:5: Well-formedness error: BlockingStatement not allowed within other BlockingStatement

BlockingStatement not allowed in interface behaviour

Events handling can be 'blocking' in component behaviour only. It is not allowed in interfaces. So:

 1  interface Sensor {
 2    in void enable();
 3    in void disable();
 4    behaviour {
 5      on enable: { ---- }
 6      blocking on disable: { ... }
 7    }
 8  }

results in the following error message:

6:5: Well-formedness error: BlockingStatement not allowed in interface behaviour

BlockingStatement not allowed with multiple provides ports

A component with more than one provides port is not allowed to block events, due to implementation restrictions. So:

  1  interface Sensor {
  2    in void activate();
  3    out void activated();
  4    behaviour {
  5      on activate: {}
  6      on inevitable: activated;
  7    }
  8  }
  9
 10  interface Test {
 11    in void test();
 12    behaviour {
 13      on test: {}
 14    }
 15  }
 16
 17  component SensorComp {
 18    provides Sensor sensor1;
 19    provides Test test;
 20    requires Sensor sensor2;
 21    behaviour {
 22      blocking on sensor1.activate(): sensor2.activate();
 23      on sensor2.activated(): { sensor1.activated(); sensor1.reply(); }
 24      on test.test(): {}
 25    }
 26  }

results in the following error message:

22:5: Well-formedness error: BlockingStatement not allowed with multiple provides ports

Well-formedness Checks — Mixing

A behaviour description introduces a sequence of statements. A statement itself can be a CompoundStatement, which is a sequence of statements between curly braces.

In order to be able to define clear semantics, there are some restrictions on the mix of statements in such a sequence.

Only declarative Statement allowed here

If a sequence starts with a declarative Statement (as in [state.Armed]---- or on console.disarm(): …​), all other statements shall be declarative Statements.

Only imperative Statement allowed here

If a sequence starts with either an imperative Statement (as in state = States.Armed; or siren.turnon();), all other statements must also be imperative.

Otherwise guard combined with second otherwise is not allowed

An otherwise guard catches the remaining cases for a list of guards. For that reason it is not allowed to have more than one otherwise statement in a list. So:

 1  on console.arm():
 2  {
 3    [sounding]  sounding = false;
 4    [otherwise] sounding = true;
 5    [otherwise] illegal;
 6  }
 7

will result in the following error message:

4:4: Well-formedness error: Otherwise guard combined with second otherwise is not allowed
5:3: Well-formedness error: Second otherwise defined here

Otherwise guard combined with non GuardedStatement is not allowed

An otherwise guard catches the remaining cases for a list of guards. For that reason it is not allowed combine an otherwise statement with a non-guarded statement. So:

 1  on console.arm(): sounding = false;
 2  [otherwise] { on console.disarm():  sounding = true; }
 3

will result in the following error message:

4:2: Well-formedness error: Otherwise guard combined with non GuardedStatement is not allowed
1:2: Well-formedness error: non GuardedStatement defined here

Illegal must be the only Statement in a compound

An illegal ActionStatement must occur on its own; no other ActionStatements or AssignmentStatements are allowed. That also applies if the illegal occurs in a nested CompoundStatement:

 1  on console.arm():
 2  {
 3    {
 4      { illegal; }
 5    }
 6    sounding = true;
 7  }

This results in the following error message:

4:7: Well-formedness error: Illegal must be the only Statement in a compound

Using illegal within a conditional statement is allowed. Also the condition may be accompanied by other action statements, e.g:

 1  on console.arm():
 2  {
 3    s = sensor.enable();
 4    if (s.NOK) {
 5      illegal;
 6    }
 7  }

Illegal is not allowed in if-then-else statements

In an Interface declaration an Event can only be declared illegal in a direct way. This is due to the declarative character of interfaces. To be more specific, it must not occur in an if-then-else construct. An example:

 1  bool b = true;
 2  on arm:
 3  {
 4    if (b) { illegal; }
 5    else   { state = States.Armed; }
 6  }

This results in the following error message:

4:12: Well-formedness error: Illegal is not allowed in if-then-else statements

Illegal is not allowed in functions

In an Interface declaration an Event can only be declared illegal in a direct way. This is due to the declarative character of interfaces. To be more specific, it must not occur in a function body. An example:

 1  void ill()
 2  {
 3    illegal;
 4  }
 5  on arm:
 6  {
 7    ill();
 8  }

This results in the following error message:

3:3: Well-formedness error: Illegal is not allowed in functions

Well-formedness Checks — Reply

A 'reply' is required in the handling of a valued (i.e. non-void) event. It is also required in case an event (that might be void) is used in 'blocking' mode; in that case the occurrence of the reply might be postponed. In general this is hard to check statically. What can be checked is described below.

Reply not allowed on 'requires' Port: 'sensor'

A 'reply' which is issued to release a blocking event refers to the event’s port. Since blocking is effective on 'provides' ports only, a well-formedness error is issued when a 'requires' port name is used. An example:

  1 component Test {
  2   provides Start start;
  3   requires Sensor sensor;
  4   behaviour {
  5    on start.start(): { sensor.activate(); }
  6    blocking on start.stop(): { sensor.activate(); }
  7    on sensor.deactivated(): { sensor.reply(); }
  8   }
  9 }

This results in the following error message:

7:32: Well-formedness error: Reply not allowed on 'requires' Port: 'sensor'

Well-formedness Checks — Valued Actions and Functions

Both Actions and Functions can be valued, and as such are considered to be expressions. The places where they can be called are severely restricted. The main reason is that Actions and Functions (at least the ones containing Actions) cause a side effect. The order of evaluation in complex expressions becomes an issue when side effects are considered. In order to exclude that, valued Actions and Function calls can only occur in isolation at the right hand side of an assignment.

An extra restriction to this rule is put on the initial value of a global variable in a behaviour. Such an expression can not contain Actions and Functions at all, since Actions are only allowed within an OnEventStatement.

Actions are not allowed here

An Action is used in a complex expression.

  1  interface Sensor {
  2    enum Status { OK, NOK };
  3    in Status enable();
  4  }
  5  component Alarm {
  6    provides Console console;
  7    requires Sensor sensor;
  8    behaviour {
  9      ----
 10      bool b = true;
 11      on console.arm():
 12      {
 13        if (sensor.enable() == Sensor.Status.OK) {
 14          state = States.Armed;
 15        }
 16        bool b = sensor.enable();
 17        bool b = b || sensor.enable();
 18      }
 19    }
 20  }

This results in the following error messages:

13:10: Well-formedness error: Actions are not allowed here
17:20: Well-formedness error: Actions are not allowed here

The call of the sensor.enable() action on line 16 is the only acceptable one.

Action is used as initial value of a global variable.

  1  interface Sensor {
  2    enum Status { OK, NOK };
  3    in Status enable();
  4  }
  5  component Alarm {
  6    provides Console console;
  7    requires Sensor sensor;
  8    behaviour {
  9      ...
 10      Sensor.Status st = sensor.enable();
 11      on console.arm():
 12      {
 13        ...
 14      }
 15    }
 16  }

This results in the following error message:

10:24: Well-formedness error: Actions are not allowed here

Function calls are not allowed here

A Function call is used in a complex expression.

  1  interface Sensor {
  2    enum Status { OK, NOK };
  3    in Status enable();
  4  }
  5  component Alarm {
  6    provides Console console;
  7    requires Sensor sensor;
  8    behaviour {
  9      ----
 10      bool ok() {
 11        return (enab() == OK);
 12      }
 13      Sensor.Status enab() {
 14        Sensor.Status r = sensor.enable();
 15        return r;
 16      }
 17      ...
 18    }
 19  }

This results in the following error message:

11:14: Well-formedness error: Function calls are not allowed here

Function value discarded: negate

A valued Function is called without assigning its return value.

  1      ...
  2      bool negate(bool b)
  3      {
  4        return !b;
  5      }
  6      void test(bool b)
  7      {
  8        negate(b);
  9      }
 10      ...

This results in the following error message:

8:7: Well-formedness error: Function value discarded: negate

Action value discarded: enable

A valued Function is called without assigning its return value. An example:

  1  interface Sensor {
  2    enum Status { OK, NOK };
  3    in Status enable();
  4  }
  5  component Alarm {
  6    provides Console console;
  7    requires Sensor sensor;
  8    behaviour {
  9      ----
 10      on console.arm():
 11      {
 12        sensor.enable();
 13      }
 14    }
 15  }

This results in the following error message:

12:7: Well-formedness error: Action value discarded: enable

Well-formedness Checks — Injection

Injected Port has out event: i

When a Component has a required injected Port, the corresponding Interface shall not have out events. An example:

 1  interface Intf {
 2    in void evt();
 3    out void notif();
 4  }
 5
 6  component Comp {
 7    requires injected Intf i;
 8    ----.
 9  }

The following error message will be issued:

7:26: Well-formedness error: Injected Port has out event: i

Well-formedness Checks — Binding

In a composite Component the Component’s ports and all sub Component ports must be bound correctly.

We’ll use the following (somewhat artificial) example to elaborate on binding errors below:

  1  import Console;
  2  import Alarm_Impl;
  3  import Sensor_Impl;
  4  import Siren_Impl;
  5
  6  component AlarmSystem
  7  {
  8    provides Console console;
  9    provides Console consoleAlt;
 10
 11    system
 12    {
 13      Alarm_Impl alarm;
 14      Sensor_Impl sensor;
 15      Siren_Impl siren;
 16
 17      // bindings ----.
 18    }
 19  }

Bindings in which 'wildcards' are involved will be described at the end of this section.

Port is not bound: console

No binding is specified for a port of a composite Component. If no bindings are added in the AlarmSystem Component above, the following error message will be issued (among others):

8:19: Well-formedness error: Port is not bound: console
9:19: Well-formedness error: Port is not bound: consoleAlt

Port is not bound: alarm.console

No binding is specified for a port of a sub Component. If no bindings are added in the AlarmSystem Component above, the following error message will be issued (among others):

12:16: Well-formedness error: Port is not bound: alarm.console

Port is bound twice: alarm.console

More than one binding is specified for a port of a composite Component or one of its sub Components. If line 17 in the AlarmSystem Component above is followed by

 18      console <=> alarm.console;
 19      alarm.sensor <=> sensor.sensor;
 20      consoleAlt <=> alarm.console;

the following error message will be issued (among others):

20:20: Well-formedness error: Port is bound twice: alarm.console

Binding directions do not match

The directions of the left and right port mentioned in the binding do not match. The following constructs are allowed:

  • When binding a port of the Component to a port of a sub Component, the directions must be the same:

    • provides binds to provides

    • requires binds to requires

  • When binding a port of the Component to another port of the Component (does this make sense??), the directions must be the opposite:

    • provides binds to requires or vice versa.

  • When binding a port of a sub Component to a port of another (or the same) sub Component, the directions must be the opposite:

    • provides binds to requires or vice versa.

If line 17 in the AlarmSystem Component above is followed by

 18      console <=> consoleAlt;

the following error message will be issued (among others):

18:5: Well-formedness error: Binding directions do not match

Binding two wildcards is not allowed

When a 'wildcard' is used in a binding the other side of the binding cannot have a wildcard also.

An example:

  1  component Sys {
  2    provides Console console;
  3    system {
  4      Logger logger;
  5      SubSystem sub;
  6      ...
  7      logger.* <=> sub.*;
  8      ...
  9    }
 10  }

This will result in the following error message:

7:14: Well-formedness error: Binding two wildcards is not allowed

Component is part of a cyclic binding

We can define communication 'direction' for bindings as follows:

  • For two sub components communicating: the requires port directs to the provides port in the binding.

  • For port forwarding (an external port is forwarded to a sub-component port) or vice versa: A provides external port directs to a provides sub-component port, and a requires sub-component port directs to a requires external port.

To prevent component re-entrancy and guarantee run-to-completion semantics, cycles in 'directed' communication are not allowed within a system component.

In the most trivial example, which creates a one-component cycle:

  1  component Comp {
  2    provides Intf prov;
  3    requires Intf req;
  4  }
  5
  6  component Sys {
  7    system {
  8      Comp c;
  9      c.prov <=> c.req;
 10    }
 11  }

the following error message will be issued:

8:5: Well-formedness error: Component is part of a cyclic binding: c

A more elaborate example creates a cycle over three components:

  1  component Comp1 {
  2    provides Intf p;
  3    requires Intf r;
  4  }
  5
  6  component Comp2 {
  7     provides Intf p1;
  8     provides Intf p2;
  9     requires Intf r1;
 10     requires Intf r2;
 11  }
 12
 13  component Sys {
 14    provides Intf p1;
 15    provides Intf p2;
 16
 17    requires Intf r1;
 18    requires Intf r2;
 19
 20    system {
 21      Comp2 c21;
 22      Comp2 c22;
 23      Comp1 c11;
 24      Comp1 c12;
 25
 26      p1 <=> c21.p1;
 27      p2 <=> c22.p1;
 28      c21.r1 <=> c11.p;
 29      c21.r2 <=> c12.p;
 30      c22.r1 <=> c21.p2;
 31      c22.r2 <=> r2;
 32
 33      c11.r <=> r1;
 34      c12.r <=> c22.p2;
 35    }
 36  }

As a result the following error messages will be issued:

21:5: Well-formedness error: Component is part of a cyclic binding: c21
22:5: Well-formedness error: Component is part of a cyclic binding: c22
24:5: Well-formedness error: Component is part of a cyclic binding: c12

Wildcard can be bound to a provided port only

Since injected Ports are always requires Ports, and a wildcard is used to bind such a Port, the other side of a wildcard binding must be a provides Port. In this example:

  1  component Comp {
  2    requires injected Logger logger;
  3    ----.
  4  }
  5
  6   component MyLogger {
  7     requires Logger logger;
  8     ...
  9   }
 10
 11 component Sys {
 12   provides Console console;
 13   system {
 14     MyLogger myLogger;
 15     SubSystem sub;
 16     ...
 17     myLogger.logger <=> *;
 18   }
 19 }

the following error message will be issued:

17:20: Well-formedness error: Wildcard can be bound to a provided port only

System composition is recursive

A system component may instantiate an arbitrary set of other components, which can be system components themselves. It is not allowed to have a self-instance neither directly nor indirectly, since that would lead to an infinite tree of components.

In the example below five system components are defined that have mutual instances. Component C1 instantiates C3, which instantiates C4, which instantiates C1.

  1  component C1 {
  2    system {
  3      C2 c2;
  4      C3 c3;
  5    }
  6  }
  7
  8  component C2 {
  9    system {
 10      C5 c5;
 11    }
 12  }
 13
 14  component C3 {
 15    system {
 16      C4 c4;
 17      C2 c2;
 18    }
 19  }
 20
 21  component C4 {
 22    system {
 23      C1 c1;
 24    }
 25  }
 26
 27  component C5 {
 28    system { } // an empty system
 29  }

All components involved in the cyclic instantiation will be report in the error messages:

1:11: Well-formedness error: System composition is recursive: 'C1'
14:11: Well-formedness error: System composition is recursive: 'C3'
21:11: Well-formedness error: System composition is recursive: 'C4'

External port must be bound to external port: r2

There is a restriction in the binding of external ports: when an external requires port of a system Component is bound, the other side of the binding must be an external requires port also (this is only possible when that is a port of a sub Component)

In the example below some errors are reported.

  1  interface I {
  2    in void e();
  3    behaviour {
  4      on e: {}
  5    }
  6  }
  7
  8  component C1 {
  9    provides I p;
 10    requires external I r1;
 11    requires external I r2;
 12    behaviour {
 13      on p.e(): {}
 14    }
 15  }
 16
 17  component C2 {
 18    provides I p;
 19    behaviour {
 20      on p.e(): {}
 21    }
 22  }
 23
 24  component S1 {
 25    provides I p;
 26    requires I r;
 27    system {
 28      C1 c1;
 29      C2 c2;
 30      p <=> c1.p;
 31      c1.r1 <=> r;
 32      c1.r2 <=> c2.p;
 33    }
 34  }
 35
 36  component S2 {
 37    provides I p1;
 38    provides I p2;
 39    requires external I r1;
 40    requires external I r2;
 41    system {
 42      S1 s1;
 43      p1 <=> s1.p;
 44      p2 <=> r2;
 45      r1 <=> s1.r;
 46    }
 47  }

the following error message will be issued on S2:

44:12: Well-formedness error: External port must be bound to external port: r2
45:5: Well-formedness error: External port must be bound to external port: r1

Well-formedness Checks — Functions

  • A Function body can only contain imperative statements, including ActionStatements. See the sections on 'Mixing' and 'Direction' above.

  • A valued Function is required to have an explicit return.

  • A return is only allowed in a function body.

  • A recursive Function is required to be tail recursive

Function does not return a value in all cases

A valued Function should return a value using the ReturnStatement. An error is issued when a return is not guaranteed. An example:

 1      bool func()
 2      {
 3        if (a && b)
 4        { return true; }
 5        else if (c)
 6        { illegal; }
 7      }

For this code fragment the following error message will be issued:

1:10: Well-formedness error: Function does not return a value in all cases: func

Return Statement not allowed here

A return Statement is restricted to Function bodies. So

 1  on sensor.disabled():
 2  {
 3    [sounding]
 4    {
 5      return; // triggers an error
 6    }
 7  }

This will cause the following error to be reported:

5:5: Well-formedness error: Return Statement not allowed here

Statement violates tail recursion in recursive Function

A function that is recursive must be tail recursive, i.e. in its body any recursive function call shall not be followed by other Statements. So

  1  component Sensor {
  2   ...
  3   behaviour {
  4     ...
  5     void f() {
  6       bool b = false;
  7       if (b) {
  8          f();
  9          b = true;
 10        }
 11      }
 12    }
 13  }

will result in the following error message:

9:9: Well-formedness error: Statement violates tail recursion in recursive Function

Remark: two functions f and g that are defined in terms of each other are considered (mutual) recursive also.

Well-formedness Checks — Data Parameters

The restrictions on Data parameters are summarised here.

Parameter type must be a data type: Code

All event parameters specified in an event declaration must be data parameters; in other words, they must have a data type. An example:

  1 interface Sensor {
  2   enum Code { ok, nok };
  3   in void activate(Code c);
  4   behaviour { ... }
}

This will result in the following error message:

3:20: Well-formedness error: Parameter type must be a data type: 'Code'

Out Parameter is not allowed for out Event

An out Event is not allowed to have an out Data Parameter. This example:

 1  interface Sensor {
 2    extern INT $int$;
 3    in void enable();
 4    in void disable();
 5    out void triggered(out INT value);
 6    out void disabled();
 7  }

will result in the following error message:

5:30: Well-formedness error: Out Parameter is not allowed for out Event: value

Inout Parameter is not allowed for out Event

An out Event is not allowed to have an inout Data Parameter. An example:

 1  interface Sensor {
 2    extern INT $int$;
 3    in void enable();
 4    in void disable();
 5    out void triggered();
 6    out void disabled(inout INT dis);
 7  }

will result in the following error message:

6:31: Well-formedness error: Inout Parameter is not allowed for out Event: dis

Parameter Binding not allowed here

Parameter binding, which is the binding of a global data variable 'D' to an event parameter 'p' using the 'p ← D' construct, is allowed in an 'on event' context only. Any other location is reported as an error. So:

  1 extern xint $int$;
  2 component Test {
  3  provides Intf intf;
  4   behaviour {
  5     xint NR;
  6     on intf.evt(number):
  7       fn(number <- NR);
  8
  9     void fn(xint i) { ... }
 10   }
 11 }

will result in the following error message:

7:17: Well-formedness error: '<-' not allowed here

If you have questions that weren’t answered by this Guide,
let our support team help you out.

Enjoy this article? Don't forget to share.
google-site-verification:google656c7703ab521151.html