We’re here to help you

Menu

Simulation and Verification Error Messages

Simulation and verification error messages

The following errors may be reported by the model simulation and by the model verification:

The following errors may be reported by the model verification:

The meaning of these errors is explained and illustrated in the following sections.


Action is illegal

Component executes an 'illegal' action statement or component executes an action statement which is 'illegal' in the current state of the port.

Example:

component ActionIsIllegal
{
  provides IA pp;
  requires IB rp;

  behaviour
  {
    on pp.ia(): rp.ia();
    on rp.oa(): illegal;
  }

  // Simulate ActionIsIllegal =>
  //   Action is illegal
  // if following trace is performed:
  //   pp.ia
  //   rp.ia

  // Simulate ActionIsIllegal =>
  //   Action is illegal
  // if following trace is performed:
  //   rp.oa
}

interface IA
{
  in void ia();

  behaviour
  {
    on ia: {}
  }
}

interface IB
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: illegal;
    on inevitable: oa;
  }
}

Trace illustrating simulation error

Trace illustrating simulation error


Completeness: EVENT reply value not set

The on-event statement for valued in-event EVENT is not able to return due to the reply value not being set.

Example:

component CompletenessReplyValueNotSet
{
  provides I pp;
  requires ISync rp;

  behaviour
  {
    on pp.ia(): rp.ia(); // Completeness:: pp.ia reply value not set
    on rp.ok(): {}
    on rp.fail(): {}
  }
  // Simulate CompletenessReplyValueNotSet =>
  //   pp.ia reply value not set
  // if following trace is performed:
  //   pp.ia
  //   rp.ia
  //   rp.ok
  //   rp.return
}

interface I
{
  in bool ia();

  behaviour
  {
    on ia: reply(true);
    on ia: reply(false);
  }
}

interface ISync
{
  in void ia();
  out void ok();
  out void fail();

  behaviour
  {
    on ia: ok;
    on ia: fail;
  }
}

Trace illustrating simulation error


deadlock in model MODEL

None of the events by which MODEL could make progress can occur.

Example:

interface DeadlockInModel
{
  in void ia();
  out void oa();

  behaviour
  {
    bool b = false;
    on ia: illegal;
    [b] on inevitable: oa;
  }
  // Simulating DeadlockInModel =>
  //   deadlock in model Deadlock
  // if empty trace is performed
}

Trace illustrating simulation error


EVENT (implicitly) illegal

Component has no model text to handle EVENT in current state. The interface of its port requires the handling of the EVENT in its current state. The port associated with EVENT is in a state where EVENT can occur. This is a case where the component does not comply with the port interface behaviour.

In a component if a combination of state and event does not have an explicit specification implicitly illegal is assumed.

Example:

component EventNotHandled
{
  provides IA pp;
  requires IB rp;

  behaviour
  {
    bool b = false;
    [b] on pp.ia(): rp.ia();
    [b] on rp.oa(): illegal;
  }

  // Simulate EventNotHandled =>
  //   pp.ia (implicitly) illegal
  // if the following trace is performed:
  //   pp.ia

  // Simulate EventNotHandled =>
  //   rp.oa (implicitly) illegal
  // if the following trace is performed:
  //   rp.oa
}

interface IA
{
  in void ia();

  behaviour
  {
    on ia: {}
  }
}

interface IB
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: illegal;
    on inevitable: oa;
  }
}

Trace illustrating simulation error

Trace illustrating simulation error

Example:

component MainProgramCompletelyEmpty
{
  provides I pp;

  behaviour
  {
  }

  // Simulating MainProgramCompletelyEmpty =>
  //   pp.ia (implicitly) illegal
  // if the following trace is performed:
  //   pp.ia
}

interface I
{
  in void ia();

  behaviour
  {
    on ia: {}
  }
}

Trace illustrating simulation error


EVENT not allowed by port PORT

Component does not comply with provides port interface behaviour.

Example:

component EventNotAllowedByPort
{
  provides IA pp;
  requires IB rp;

  behaviour
  {
    on pp.ia(): {}
    on rp.oa(): pp.oa();
  }

  // Simulating EventNotAllowedByPort shall report error
  //   pp.oa not allowed by port pp
  // for trace
  //   rp.oa
  //   pp.oa
}

interface IA
{
  in void ia();
  out void oa();

  behaviour
  {
    bool b = false;

    on ia: b = true;
    [b] on optional: {b = false; oa;}
  }
}

interface IB
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on optional: oa;
  }
}

Trace illustrating simulation error


Function actual parameter declaration failed. Range error for variable PARAMETER

Value assigned to PARAMETER is outside valid value range for its type.

Example:

interface FunctionActualParameterDeclarationFailed
{
  in void ia();

  behaviour
  {
    subint Count {0..5};
    void fn(Count c) {}

    on ia: fn(6);
  }
  // Simulating FunctionActualParameterDeclarationFailed =>
  //   Function actual parameter declaration failed. Range error for variable c
  // if the following trace is performed:
  //   ia
}

Trace illustrating simulation error


Global variable declaration failed. Range error for variable VARIABLE

Value assigned to VARIABLE is outside valid value range for its type.

Example:

interface GlobalVariableDeclarationFailed
{
  in void ia();

  behaviour
  {
    subint Count {0..5};
    Count c = 6;

    on ia: c = 0;
  }

  // Simulate GlobalVariableDeclarationFailed =>
  //   Global variable declaration failed. Range error for variable c
  // if empty trace is performed
}

Trace illustrating simulation error


Illegal value in assignment: Range error for variable VARIABLE

Value assigned to VARIABLE is outside valid value range for its type.

Example:

interface IllegalValueInAssignment_IAssignmentStatement
{
  in void ia();

  behaviour
  {
    subint Count {0..5};
    Count c = 0;

    on ia: c = 6;
  }

  // Simulate IllegalValueInAssignment_IAssignmentStatement =>
  //   Illegal value in assignment: Range error for variable c
  // if the following trace is performed:
  //   ia
}

Trace illustrating simulation error

Example:

interface IllegalValueInAssignment_IReturnStatement
{
  in void ia();

  behaviour
  {
    subint Count {0..5};
    Count Init() {return 5 + 1;}
    Count c = 0;

    on ia: c = Init();
  }

  // Simulate IllegalValueInAssignment_IReturnStatement =>
  //   Illegal value in assignment: Range error for variable c
  // if the following trace is performed:
  //   ia
}

Trace illustrating simulation error

Example:

component IllegalValueInAssignment_AssignmentStatement
{
  provides I pp;

  behaviour
  {
    subint Count {0..5};
    Count i = 0;

    on pp.ia(): i = 6;
  }

  // Simulate IllegalValueInAssignment_AssignmentStatement =>
  //   Illegal value in assignment: Range error for variable i
  // if the following trace is performed:
  //   pp.ia
}

interface I
{
  in void ia();

  behaviour
  {
    on ia: {}
  }
}

Trace illustrating simulation error

Example:

component IllegalValueInAssignment_ReturnStatement
{
  provides I pp;

  behaviour
  {
    subint Count {0..5};
    Count Init() {return 6;}
    Count i = 0;

    on pp.ia(): i = Init();
  }

  // Simulate IllegalValueInAssignment_ReturnStatement =>
  //   Illegal value in assignment: Range error for variable i
  // if the following trace is performed:
  //   pp.ia
}

interface I
{
  in void ia();

  behaviour
  {
    on ia: {}
  }
}

Trace illustrating simulation error

Example:

component IllegalValueInAssignment_ActionExpressionReturn
{
  provides I pp;
  requires IDozen rp;

  behaviour
  {
    subint Count {0..5};
    Count i = 0;

    on pp.ia(): i = rp.ia();
  }

  // Simulate IllegalValueInAssignment_ActionExpressionReturn =>
  //   Illegal value in assignment: Range error for variable i
  // if the following trace is performed:
  //   pp.ia
  //   rp.ia
  //   rp.12
}

interface I
{
  in void ia();

  behaviour
  {
    on ia: {}
  }
}

interface IDozen
{
  subint Dozen {12..12};
  in Dozen ia();

  behaviour
  {
    on ia: reply(12);
  }
}

Trace illustrating simulation error


Invalid event trace

Model is not capable of performing the trace due to port or event names not valid for the simulated model or due to an invalid order of events. This error is reported if the trace does not touch an error in the model. This situation can not occur during interactive simulation. It can be reached by directly pasting a trace into the 'Trace' window and pressing the 'Update Simulation' button. It can also occur in thecommand-line 'dzn run' command.

Example:

component InvalidEventTrace
{
  provides I pp;

  behaviour
  {
    on pp.ia(): {}
  }

  // Simulating InvalidEventTrace =>
  //   Invalid event trace
  // if the following trace is performed:
  //   oa
}

interface I
{
  in void ia();

  behaviour
  {
    on ia: {}
  }
}

Trace illustrating simulation error


livelock in model MODEL

Model is caught in an endless loop from which it is unable to escape.

Example:

The component LivelockInModel defines a function 'fn' which recursively calls itself. The resulting infinite recursion will be reported as a live-lock.

component LivelockInModel
{
  provides I pp;

  behaviour
  {
    void fn() {fn();}

    on pp.ia(): fn();
  }
  // Simulating component 'LivelockInModel' =>
  //   Livelock in model LivelockInModel
  // if the following trace is performed:
  //   pp.ia
}

interface I
{
  in void ia();
  behaviour
  {
    on ia: {}
  }
}

Trace illustrating simulation error


MODEL is incomplete: 'EVENT' not handled

Interface has no handling for EVENT in current state.

Example:

interface IBehaviourEmpty
{
  in void ia();

  behaviour
  {
  }
  // Simulate IBehaviourEmpty =>
  //   IBehaviourEmpty is incomplete: 'ia' not handled
  // if the following trace is performed:
  //   ia
}

Trace illustrating simulation error


Out-events on provides port PORT_B not allowed. Only out-events on provides port PORT_A allowed in current call context.

An in-event on a provides port is not allowed to refine a modelling event on another provides port. Consequently, the on-event statement for an in- event on a provides port may not contain an action statement for an out- event on another provides port.

Example:

component OutEventsOnProvidesPortNotAllowed
{
  provides I ppa;
  provides I ppb;

  behaviour
  {
    on ppa.ia(): ppb.oa();
    on ppb.ia(): ppa.oa();
  }

  // Simulating OutEventsOnProvidesPortNotAllowed
  //   Out-events on provides port PORT_B not allowed. Only out-events on
  //   provides port PORT_A allowed in current call context.
  // if the following trace is performed:
  //   ppa.ia
  //   ppb.oa
}

interface I
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on optional: oa;
  }
}

Trace illustrating simulation error

Trace illustrating simulation error


Reply not allowed: port PORT not blocked.

A reply statement for a port which is not currently blocked.

A reply statement enables a call return. The blocked call which will be released as a result of the reply statement is either the current provides port in-event call or a prior 'blocking' provides port in-event call for which the reply statement has not been executed yet.

Example:

component ReplyNotAllowedPortNotBlocked
{
  provides I pp;
  requires I rp;

  behaviour
  {
    on pp.ia(): {}
    on rp.oa(): pp.reply();
  }

  // Simulating ReplyNotAllowedPortNotBlocked =>
  //   Reply not allowed: port 'pp' not blocked.
  // if the following trace is performed:
  //   rp.oa
}

interface I
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on inevitable: oa;
  }
}

Trace illustrating simulation error


Reply not allowed on requires-port: PORT

The on-event statement for a requires port out-event is processed in a call context which is abstracted away. The return of that call context may not be specified in the interface model.

Example:

component ReplyNotAllowedOnRequiresPort
{
  provides I pp;
  requires I rp;

  behaviour
  {
    on pp.ia(): {}
    on rp.oa(): reply();
  }
  // Simulating ReplyNotAllowedOnRequiresPort =>
  //   Reply not allowed on 'requires' port: 'rp'
  // if the following trace is performed:
  //   rp.oa
}

interface I
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on optional: oa;
  }
}

Trace illustrating simulation error


Reply not allowed for 'optional' or 'inevitable'

'optional' and 'inevitable' are abstractions of a call context in which an action is performed. The return of that call context is abstracted away and may not be specified in the interface model.

Example:

interface ReplyNotAllowedForModellingEvent
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on optional: {oa; reply();}
  }
  // Simulating ReplyNotAllowedForModellingEvent =>
  //   Reply not allowed for modelling event
  // if the following trace is performed:
  //   oa
}

Trace illustrating simulation error


Reply statement does not match event return type.

The value passed into the reply statement does not match the return type of the valued in-event for which it will serve as a return value.

Example:

component ReplyStatementDoesNotMatchReturnType
{
  provides IB pp;
  requires I rp;

  behaviour
  {
    on pp.ia(): blocking rp.ia();
    on rp.oa(): pp.reply(12);
  }
  // Simulating ReplyStatementDoesNotMatchReturnType =>
  //   Reply statement does not match event return type.
  // if the following trace is performed:
  //   pp.ia
  //   rp.ia
  //   rp.oa
  //   rp.return
}

interface IB
{
  in bool ia();
  behaviour
  {
    on ia: reply(false);
  }
}

interface I
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: oa;
  }
}

Trace illustrating simulation error

Example:

interface IReplyStatementDoesNotMatchReturnType
{
  in bool ia();

  behaviour
  {
    on ia: reply(12);
  }
  // Simulating IReplyStatementDoesNotMatchReturnType =>
  //   Reply statement does not match event return type.
  // if the following trace is performed:
  //   ia
}

Trace illustrating simulation error


Void reply not allowed in non-blocking action.

A void reply statement is only allowed in the context of the current void in-event call if the action is marked as 'blocking'.

A reply statement enables a call return. The blocked call which will be released as a result of the reply statement is either the current provides port in-event call or a prior 'blocking' provides port in-event call for which the reply statement has not been executed yet.

Example:

component SpuriousVoidReplyStatement
{
  provides I pp;

  behaviour
  {
    on pp.ia(): reply();
  }
  // Simulating SpuriousVoidReplyStatement =>
  //   Void reply not allowed in non-blocking action.
  // if the following trace is performed:
  //   pp.ia
}

interface I
{
  in void ia();

  behaviour
  {
    on ia: {}
  }
}

Trace illustrating simulation error


Component COMPONENT is non-deterministic due to overlapping guards

The component COMPONENT has multiple different on-event statements for the same event in the same state.

Example:

component ComponentIsNonDeterministic
{
  provides I pp;

  behaviour
  {
    [true] on pp.ia(): pp.oa();
    [true] on pp.ia(): pp.ob();
  }

  // Verifying model ComponentIsNonDeterministic =>
  //   Component ComponentIsNonDeterministic is non-deterministic due to overlapping guards
  // For trace
  //   pp.ia
}

interface I
{
  in void ia();
  out void oa();
  out void ob();

  behaviour
  {
    on ia: {}
  }
}

Trace illustrating verification error


EVENT not performed by component

Component does not comply with provides port interface behaviour. Interface requires component to perform EVENT while component refuses to do so.

Example:

component ComponentIsNonCompliantWithInterface
{
  provides I pp;

  behaviour
  {
    on pp.ia(): {}
  }

  // Verifying ComponentIsNonCompliantWithInterface =>
  //   pp.oa not performed by component
  // for trace
  //   pp.ia
  //   pp.return
}

interface I
{
  in void ia();
  out void oa();

  behaviour
  {
    bool b = true;
    [b] on ia: b = false;
    [!b] on ia: illegal;
    [!b] on inevitable: {oa; b = true;}
  }
}

Trace illustrating verification error


MODEL is incomplete: EVENT not handled

The interface model MODEL does not handle EVENT in its current state.

Example:

interface ModelIsIncomplete
{
  in void ia();

  behaviour
  {
    bool b = true;
    [b] on ia: b = false;
  }

  // Verifying model ModelIsIncomplete =>
  //   ModelIsIncomplete is incomplete: 'ModelIsIncomplete.ia' not handled
  // for trace
  //   ia
  //   return
}

Trace illustrating verification error


queue full

The queue size limit used during verification is exceeded. (dzn verify -q )

Example:

component QueueFull
{
  provides IP pp;
  requires IR rp;

  behaviour
  {
    on pp.ia(): rp.ia();
    on rp.oa(): {}
  }

  // Verifying model QueueFull =>
  //   queue full
  // For trace
  //   pp.ia
  //   rp.ia
  //   rp.oa
  //   rp.oa
  //   rp.oa
  //   rp.oa
  //   rp.return
}

interface IP
{
  in void ia();

  behaviour
  {
    on ia: {}
  }
}

interface IR
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {oa; oa; oa; oa;}
  }
}

Trace illustrating verification error

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.