Note

You are not reading the most recent version of this documentation. 1.4.7 is the latest version available.

Release Notes

1.1.3 (17/05/2022)

Bug fixes:

  • Fixes an issue that would prevent the generated C++ code from compiling using g++4.4 if the Coco code needed to default a variable of type Result<E, _> where E is a simple enum.

1.1.2 (04/05/2022)

Bug fixes:

  • Fixes an issue that would cause incorrect runtime behaviour when writing match statements that contained only a single wildcard clause. For example:

    match (e) {
  _ => f,
}

    In the generated code, e would not be evaluated meaning that any side-effects in e would be lost. This only happens in the above case, where the match expression contains one clause with a _ as the pattern.

1.1.1 (02/04/2022)

All users are advised to upgrade to this version immediately due to the first bugfix below, which could result in different behaviour between the generated code and the verified model. Upon upgrading, we recommend re-verifying all models to see if any new invalid behaviour is detected.

Bug fixes:

  • Fixes an issue that would cause incorrect behaviour during verification when using || in combination with calls on required ports. Specifically, if a model contained a statement of the form:

    if (x || y) e

    where either x or y contains a function call on a required port, then in the case that x evaluates to true, e would not be executed.

  • Fixes an issue that would prevent compilation of the generated mocks if ports used functions that returned Result.

1.1.0 (30/11/2021)

This is the first point release of Coco 1.x. It contains no backwards-incompatible changes compared to 1.0, except for some minor bug fixes to the typechecker that ensure that invalid models are correctly rejected. Such scripts would have resulted in Coco’s verification failing with internal errors.

New features:

  • A new state machine structure viewer has been added to the Coco plugin for Eclipse. This provides an easy way to see a summary of which events are allowed in which states. The structure viewer is also used to display reachability data from the verification, providing an easier-to-use visualisation than the existing state diagram visualisation. This is only an initial release and more features will follow.

  • Static constants can now be defined in states, structs, enums, ports and components. For example:

    port Driver {
  static val kInitialized : Int = 10
}

  • The C generator has undergone major improvements and now supports far more of Coco.

  • The architecture diagram incorporates many improvements that should result in more readable diagrams, including:

    • Highly-connected ports are now shown as references rather than edges.
    • Comments from declarations are now shown in the tooltips when hovering over a node.
    • Performance on large diagrams has been improved.

  • Added generator.cpp.componentStyle to provide an additional mode for generating C++ code for components that is designed to improve compilation times on large components by generating code using a pImpl-like pattern.

  • The cloud verification has been improved to provide better responsiveness, meaning that jobs should start more quickly, particularly when the service is under heavy load.

Improvements:

  • Coco’s gmock_helpers.h header now includes some additional matchers to assist with matching values of type coco::optional or coco::expected, making it easier to construct gMock-based tests.
  • The Coco generated mocks now expose the normally protected port fields (e.g. for a required port r, the field would be called r_) to allow the send_ methods to be directly accessed to ease construction of asynchronous mocks.
  • Functions marked with @noSideEffects can now be used inside state invariants.
  • The command-line output now includes a summary of how many errors were encountered.
  • Added support for using COCOTEC_AUTH_TOKEN together with the coco binary to directly invoke Coco using a machine authentication token.
  • Fixes a case where Coco would incorrectly allow components that used _ inside implicit member expressions.
  • Fixes a case where some unusual architectures were incorrectly allowed with missing setAccess calls.
  • Added support for converting States to String via Cast: e.g. nextState as String.
  • Non-verified fields of structs can now be referenced without preventing verification.
  • Defaulted type parameters are now correctly applied when looking up static constants. For example, given struct S<T = Int> {…}, then S.x will look for static members in S<Int>.
  • Member functions inside external types, structs, and enums can now use the binaryOperator, implicitCast, and unaryOperator attributes.
  • The Java API can now override the path to the license file, allowing for easier integration with CI pipelines.
  • Coco’s license server can now be run on-premise, providing another option for running Coco in environments with no internet connectivity in addition to the pre-existing offline licenses.

Bug fixes:

  • Fixes a case where the generated code would mistakenly elide sub-expressions with side effects when using the Result.discard function.
  • Fixes a crash when generating code that uses Result.value in certain combinations.
  • Fixes a crash when running Eclipse for more than 24 hours whilst using the remote verification.
  • Fixes a crash when typechecking files that used implicit member expressions on values of type Signal where the signals had parameters.
  • Fixes an issue that would cause text to be incorrectly sized on the architecture, state, and counterexample diagrams on Linux.
  • Fixes a problem where incorrect include extensions would be created when generating code.
  • Fixes an issue with sizing the swimlane columns in the counterexample viewer on Linux.
  • Fixes an issue that prevented using coco --no-license-server with an on-premise license token.
  • Fixes a crash when viewing counterexamples where the provided port events include a return with an enum.
  • Fixes a case where the C generator would generate uncompilable C code when passing a Slot<T> to a function of type &out T.
  • Fixes a case where the C generator would generate uncompilable C code when dereferencing via multiple fields (e.g. x.y.z).
  • Fixes a case where the typechecker would fail, but no diagnostics would be reported.
  • Fixes a case where the verification would report an internal error when a function inside a state machine returns a value that is then immediately implicitly cast.
  • Fixes a case where vals of type Bounded would not have their bounds checked on initialisation.
  • Fixes a bug where the support bundle command would incorrectly mangle the names of modules.

1.0.6 (21/10/2021)

Bug fixes:

  • Fixes an issue when using the remote verification service that would result in the disconnected icon incorrectly appearing.

1.0.5 (11/10/2021)

Bug fixes:

  • Fixes an issue that would result in the command-line tools being unable to generate state or architecture diagrams.
  • Fixes an internal error when verifying models that use struct literals including undefined expressions.
  • Fixes a case where generating code for a project that contains verification warnings could generate C++ code that would not compile.
  • Fixes several code generation issues with multi-threaded encapsulating components that wrap single-threaded components, and would have resulted in the generated code not being compilable.

1.0.4 (29/09/2021)

Bug fixes:

  • Fixes a case where offline licenses would expire after only 24 hours.
  • Fixes a case where acquiring a license on Linux from the command-line would fail to open the browser or give any error messages.
  • Fixes a crash when viewing counterexamples where the provided port events include a return with an enum.
  • Fixes a warning when compiling Coco-generated C++ code using MSVC.

1.0.3 (16/09/2021)

Bug fixes:

  • Fixes a case where the Terminated state would be incorrectly marked as unreachable. This would cause the count of unreachable states in Eclipse to be off by 1.
  • Fixes several warnings when compiling Coco-generated C++ code using MSVC.
  • Fixes a case where the coco::SingleThreadedGMockHelper would fail to fire a pending timer transition.

1.0.2 (15/09/2021)

Bug fixes:

  • Fixes a case where cloud verification would fail with an error saying that the verification server was unreachable.
  • Fixes an issue with both coco::MultiThreadedGMockHelper and coco::SingleThreadedGMockHelper that could cause calls to InvokeAsync() that specified a timeout to never be invoked.
  • Fixes a case where external components with required ports would be generated using non-pure-virtual methods.
  • Fixes a case where the pretty-printer would incorrectly qualify signal names when sending a signal within a base port.
  • Fixes a case where the remote verification would not correctly load results from the verification cache, leaving the assertion marked as not started in the assertions tree.

Minor improvements:

1.0.1 (09/09/2021)

Bug fixes:

  • Fixes a case where remote verification would fail due to expired authentication credentials.
  • Fixes a crash when attempting to obtain a license whilst there is no internet connection.
  • Fixes a bug that would cause proxies to be incorrectly detected on Linux.
  • Fixes a bug that cause leaf verification status icons to not be marked as unknown after editing a file.
  • Fixes generation of C++ mocks that include array indexes.
  • Fixes a case where verification of single-threaded components that use timers and also have shared required ports could fail with spurious counterexamples about deadlocks.
  • Fixes a bug that would cause single-threaded encapsulating components with incorrect setAccess calls to be accepted.
  • Fixes a case where forward declarations would not be correctly created when generating C++ code.
  • Fixes the location of gmock_helpers.h and moves it to generator.cpp.testOutputDirectory.
  • Fixes a case where immutable references would not require an explicit reference.
  • Fixes a crash when a function call contains an invalid argument.
  • Fixes a bug that would cause Coco to require re-authorisation every 24 hours.

1.0.0 (15/08/2021)

This release marks the first stable release of the Coco Platform. In particular, this release stabilises:

  • The core Coco Language;
  • The C++ generator;
  • The command-line tooling.

Future releases will follow semantic versioning, meaning that releases of the form 1.x will not introduce backwards-incompatible changes (except to fix bugs). Further, support for 1.x will be provided even after the release of 2.x.

The release notes for the betas and release candidates that led up to 1.0.0 can be found at 1.0 Pre-Releases. Relative to the final release candidate, this release contains the following changes:

Breaking changes:

  • In the generated C++ code, the generated classes corresponding to Required<P> no longer contain default implementations of methods to receive signals, meaning that any subclass must now override all signal receptions.
  • Custom trait instances of Default must now define default() as an external function. This is to ensure that it is clear that this function is only relevant during verification, and not in the generated code.

Improvements:

  • Implicit member expressions can now be used for setAccess, setAllow, setUnique, and Signal.
  • The reachability results highlighting on the state diagram viewer has been improved to more clearly show which states and transitions are unreachable. Further, several bugs were fixed that would result in misleading results being presented.
  • The architecture diagram and state machine diagram now support more intuitive navigation, and can be panned by dragging, and zoomed using the scroll wheel.
  • The support-bundle command has been added to Eclipse, to allow projects to be obfuscated and sent to Coco support.
  • Coco’s C++ logging can now be enabled project wide using the generator.cpp.alwaysEnableLogging setting. This means that COCO_LOGGING_ENABLE no longer needs to be defined when this setting is enabled.
  • generator.cpp.outputEmptyFiles has been added to control whether Coco should generate empty files for each input .coco file, even if that file does not contain any codegen-relevant definitions.
  • generator.cpp.runtimeHeaderFileExtension has been added to control the file extension that the Coco runtime should be generated with.
  • The licensing system now supports granting licenses to machines that have no internet connectivity, and also cannot be granted fixed licenses (e.g. build machines).

Bug fixes:

  • Fixes a crash when viewing counterexamples for anonymous state machines.
  • Fixes several minor issues where the architecture diagram would highlight the wrong nodes on hover.
  • Fixes a crash when defining files inside folders whose names are a Coco keyword.
  • Fixes a case where the verification would erroneously fail on models that used PortAccess.Shared with the mixed runtime.
  • Fixes an issue that prevented the generated code from compiling if multiple single-threaded components were connected to the same multi-threaded required port on a boundary of an encapsulating component.
  • Fixes several cases where diagnostics would be created about @unbounded spontaneous transitions, but the overall operation was not marked as a failure.
  • Fixes a typechecker error that resulted in State being incorrectly marked as comparable for equality, leading to internal errors during verification.
  • Fixes an internal error when passing literal integers to parameters of type NonVerified<Int>.
  • Fixes a case where assignments to non-verified variables would result in verification side-effects being omitted.
  • Fixes a case where verified values could not be assigned to elements of a non-verified array.
  • Fixes an issue when using state machine inheritance that resulted in transitions in the base state machine from always being marked as unreachable.
  • Fixes an issue that would cause required ports that contain unbounded spontaneous transitions but no function calls to sometimes incorrectly pass the responsiveness check.
  • Fixes an issue that would cause single-threaded components that require ports with unbounded spontaneous transitions to deadlock during verification, leading to false counterexamples.
  • Fixes an issue that would lead to internal errors being raised when verifying state machines that use unsubscribe during init().
  • Fixes an issue that prevent the compilation of the generated code when using external components with arrays of provided ports.
  • Fixes an issue that prevent the compilation of the generated code when using arrays of provided ports on multi-threaded encapsulating components that contain single-threaded components.
  • Fixes several issues that prevent coco::expected from being used conveniently in hand-written code, particular when using older C++ compilers.
  • Fixes an issue that caused gmock_helpers.h to be inserted into the normal generated code folder, rather than the test-specific one.
  • Fixes an oversight that led to SingleThreadedTimerExecutor not having a virtual destructor.