Migrating to Coco 1.0.0¶

Derive¶

Coco no longer automatically derives Default for structs or tagged enums or Eq for tagged enums (simple enums are unaffected) and requires the @derive attribute to be specified instead. This will affect any tagged enums or structs that you have defined and will typically result in error messages like:

no default value is known for type E; either give an explicit initialiser, use a Slot<E>, or define an instance of Default(E)

cannot compare E and E; could not find an instance of Eq(E) or NonVerifiedEq(E)

To fix this, add @derive(Default) or @derive(Eq) (or @derive(Default, Eq)) to the declaration of the enum or struct:

@derive(Default, Eq)
enum E { ... }

@derive(Default)
struct S { ... }

BoundedInt¶

In addition to Coco’s BoundedInt type being replaced by the new Bounded type, which is automated, BoundedInt is also no longer implicitly convertible to Int, or to other BoundedInt types. For example, all of the following would now be rejected:

function fn(x : Int) : BoundedInt<0, 2> = x
function fn(x : BoundedInt<0, 3>) : BoundedInt<0, 2> = x

To fix this, explicit conversions can be used:

function fn(x : Int) : BoundedInt<0, 2> = x as BoundedInt<0, 2>
function fn(x : BoundedInt<0, 3>) : BoundedInt<0, 2> = x as BoundedInt<0, 2>

We recommend that rather than using BoundedInt<0, 5> directly, you instead create a type alias that gives a meaningful name to the range:

type DeviceId = BoundedInt<0, 5>

This will make the casts easier to write and understand.

Spontaneous verification¶

A port is no longer allowed to perform an infinite sequence of empty spontaneous transitions, where an empty spontaneous transition is one that does not send any signals, or alter the state. This is now verified as part of the well-formedness checks on ports under a new assertion called No empty spontaneous.

The following example port will fail this verification check:

port P1 {
  function f() : Nil
  outgoing signal sig()
  machine M {
    var p : Bool = true
    f() = { p = false; }
    spontaneous = {
      if (p) sig()
    }
  }
}

To fix this verification error, empty spontaneous transitions must be manually removed when they are identified via the verification. The most common cause of this will be spontaneouses like the above: to fix this, move the predicate to the outside of the spontaneous:

if (p) spontaneous = sig()

Abstracted¶

The type Abstracted has now been removed from Coco. Instead of using Abstracted<From, To>, instead define an external type that contains a member of type To. For example, suppose we previous had:

type AbstractSequenceNumber = Bounded<0, 5>
type SequenceNumber = Abstracted<Int, AbstractSequenceNumber>

This can be replaced by:

@derive(Default, Eq)
@CPP.mapToType("int", .Value)
external type SequenceNumber {
  var x : AbstractSequenceNumber
}

If an external function had an argument s of type SequenceNumber, then the external function can now be modified to use s.x instead.

Compatible¶

Port inheritance now requires the @compatible attribute to be used in order to specify which runtimes a port is compatible with. In particular, any port that inherits a port with a state machine will now give an error like:

a port that inherits from another port must declare what runtimes it is usable in using the @compatible(…) attribute

To fix this, add @compatible(.SingleThreaded), @compatible(.MultiThreaded), or even @compatible(.MultiThreaded, .SingleThreaded) to the derived port. For example:

port Base { ... }

@compatible(.MultiThreaded)
port Derived : Base { ... }

@compatible only has to be specified for ports with state machines.

Termination¶

The undocumented unsafeAutomaticTermination option has been removed in place of automatic safe termination by default.

Syntax¶

Coco’s syntax has been changed with the aim of reducing confusion over where ; are required or whether ‘;’ is a separator or a sequencing operator, and also improve the consistency of the language.

An enum declaration no longer uses ; as a separator, and instead uses the keyword case to denote each enum case. For example:

enum E {
  A;
  B(x : Int);
}

is now written as:

enum E {
  case A
  case B(x : Int)
}

Structs, ports and components have all been altered to use the same same syntax as variable declaration in state machines, as each Field is now prefixed with var or val. For example:

struct S {
  f : Int;
}

port P {
  left : L;
}

component C {
  p : D;
}

becomes:

struct S {
  var f : Int
}

port P {
  val left : L
}

component C {
  val p : D
}

Port and component fields must always be marked as immutable using val (since they are immutable references to mutable objects), whereas struct fields must currently always be marked using var.

Match expressions, offer handlers, and nondet expressions now use , as a separator instead of ;. For example, suppose we previously had:

match (m) {
  Message.Empty => -1;
  Message.Data(d) => d;
}

f(level : Bounded<0,6>) = offer {
  if (level < 2) low();
  if (level > 3) high();
  otherwise medium;
}

check() = nondet { true; false; }

These are now written as:

match (m) {
  .Empty => -1,
  .Data(d) => d,
}

f(level : Bounded<0,6>) = offer {
  if (level < 2) low(),
  if (level > 3) high(),
  otherwise medium,
}

check() = nondet { true, false, }

Queue Control¶

The following queue control functions have been renamed to improve consistency:

• setFilter has become setAllow;
• unique has become setUnique;
• setShared has become setAccess.
• The enum case None of type PortAccess, which is passed as an argument to setAccess (previously setShared has been renamed to OtherOnly.

For example, suppose we previously had:

setShared(source.monitor, PortAccess.None)

This is now replaced with:

setAccess(source.monitor, PortAccess.OtherOnly)

In addition, setAllow (previously called setFilter) is now variadic, meaning that setFilter(r, [s1, s2]) is now written as setAllow(r, s1, s2).

C++ attributes¶

The C++ attributes, @CPP.include, @CPP.mapToType, and @CPP.mapToValue have all been modified to take a variable number of parameters, rather than a list of headers. Therefore:

@CPP.mapToValue("kValue", [CPP.Header.User("header.h")])

can now be written as:

@CPP.mapToValue("kValue", CPP.Header.User("header.h"))

or even:

@CPP.mapToValue("kValue", .User("header.h"))

using implicit member expressions.

Slot members¶

The Coco Slot<T> type used to provide several functions that could be used as follows:

var s : Slot<Bool>;
isValid(s);
isInvalid(s);
invalidate(&s);
initialise(&s);

These have now been converted into member functions and so are written as:

var s : Slot<Bool>;
s.isValid();
s.isInvalid();
s.invalidate();
s.initialise();

Runtime Attribute¶

If the runtime attribute was not specified, then Coco used to assume that the component should use the MultiThreaded runtime. Due to the fact that Coco permits runtimes to be mixed, this was a common source of confusion. Therefore, the runtime attribute is now mandatory on all components.

BoundedInt¶

In addition to the changes outlined above, Coco’s BoundedInt<l, u> type has been replaced by Bounded<l, u-1>. The automatic transformation will convert all uses of Bounded to BoundedInt, converting the upper bound as necessary.