Note

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

Release Notes¶

1.2.19 (14/03/2023)¶

Bug fixes:

Fixes a rare crash when verifying models that used a lot of data.
Fixes the behaviour of the command-line tool when coco is invoked with a relative file path.
Fixes an incorrect diagnostic raised when verifying models that contain struct literals that are using type aliases.

1.2.18 (23/01/2023)¶

This is a small bugfix release to fix some packaging issues with the VSCode plugin. Users are advised to reinstall any the Coco plugin from the VScode marketplace in order to ensure they are using the correct version.

1.2.17 (23/01/2023)¶

Bug fixes:

Fixes an issue with the JUnit output from the verification which would cause fatal verification errors (e.g. could not connect to the verification server) to be reported as passes.
Fixes a crash when verifying arrays of ports that are heavily nested.
Fixes a bug in gmock_helpers.h that would cause timers to sleep for far too long when used with compilers that did not support nanosecond-precision timers.
Fixes an issue that prevented some forms of @eventually from using anything other than the literals true or false as the argument for when the property is enabled.
Fixes an issue that prevented @eventually with a boolean argument from working with offer.
Fixes an internal error when verifying nested ports that use inheritance several times.

1.2.16 (19/12/2022)¶

Bug fixes:

Fix a case where Coco would incorrectly refuse to generate C++ code due to potential conflicts in the generated code. This would occur when a function was defined within a nested declaration such as a struct or enum, and also declare at the top-level of a file.
Fix a case where the generated C++ code would misplace the forward declarations and place them at the end of the file, rather than the start. This would only affect code where a single file contained code in several different namespaces.
Fixes a case where the typechecker would incorrectly allow immutable slots to be passed to functions expecting mutable references.

1.2.15 (07/12/2022)¶

Improvements:

Implemented a small improvement to the logic added in 1.2.13 to qualify names in the generated C++ code. This should result in fewer additional qualifications and therefore fewer changes to the generated code versus previous releases.

Bug fixes:

Fix a crash when launching the simulator on User2.

1.2.14 (28/11/2022)¶

This is a re-release of 1.2.13 to fix an issue with the releases being incorrectly signed.

1.2.13 (26/11/2022)¶

Bug fixes:

Fixes a bug that would prevent @derive(Default) from being used on generic types that defaulted their generic parameters.
Fixes an issue that meant the generated C++ stubs for external components would not include parameter names.
Fixes an issue that could cause the generated C++ to contain syntax errors when using member functions on generic structs.
Fixes an issue with the generated C++ code that would cause the generated code to incorrectly qualify names, which could sometimes lead to the code being uncompilable.
Fixes an issue that would cause incorrect errors to be raised during verification about accessing fields of non-verified structs.
Fixes an issue that would cause incorrect errors about overlapping source directories in the Coco.toml file. This also fixes a case where overlapping directories would not be correctly detected, particularly when using relative paths starting with ...
Fixes an issue that would cause User2 to be misleadingly shown in reachability counterexamples.

1.2.12 (04/11/2022)¶

Bug fixes:

Improves the compatibility of the object-orientated C runtime with the C99 standard.
Fixes a memory leak in the generated code when using the object-orientated C runtime with composite ports.
Fixes a case where includes were not included correctly in the generated C++ code when using trait instances defined in modules that are separate to the type the trait instance is defined over.

1.2.11 (26/10/2022)¶

This is a primarily re-release of 1.2.10 due to a mistake in the release which meant that the fix for the first issue listed under 1.2.10 was not actually applied. Thus this release fixes the issue:

Fixes a deadlock in the generated C++ code when manually calling coco_shutdown() outside of a Coco-initiated event handler on an external component with a queue, required ports, but no provided ports.

Additional bug fixes:

Improves forward compatibility of code generated with standard = "G++4.4" with modern C++ commpilers.
Fixes a rare crash when verification fails with a counterexample that includes stepping through a for loop that contains a match with a guard on one case.

1.2.10 (21/10/2022)¶

Bug fixes:

Fixes a deadlock in the generated C++ code when manually calling coco_shutdown() outside of a Coco-initiated event handler on an external component with a queue, required ports, but no provided ports.
Fix an internal error when verifying models that use struct literals for non-verified structs.
Fix an issue with the architecture diagram that could cause ports to overlap under certain conditions.

1.2.9 (26/09/2022)¶

Bug fixes:

Fix crash when generating C++ code when @derive(NonVerifiedEq) is used.
Improve compatibility of the C++ runtime with GCC 4.9.
Fix a missing override specifier on coco::VariableSizeSingleThreadedTimerExecutor.
Fix an error when attempting to export a module from Coco to EMF that included attributes.

1.2.8 (13/09/2022)¶

Bug fixes:

Fix a crash when drawing architecture diagrams that included external implementation components whose parents used setAccess.
Fix an occasional crash when using function pointers as state parameters.

1.2.7 (22/08/2022)¶

Bug fixes:

Fix a crash when using mapToEnum on C++ enum classes.
Fix a case where the language server would not report any errors, but the command-line tool would when using external code expressions.

1.2.6 (19/08/2022)¶

Bug fixes:

Fixes an internal error whilst verifying that would prevent verification of models that used both Slot<T> and Slot<NonVerified<T>>.
Fixes an issue that would cause Testing.Mock and Testing.StrictMock to not inherit the setAccess calls from the base external component.
Fixes an issue with the VSCode plugin’s packaging that would have allowed it to be installed in a VSCode that was too old to actually run the plugin.
Fixes an issue that could have caused the verification to incorrectly fail when using slots inside structs with member functions that attempt to update the slot.
Fixes an incompatibility with some C++ static analysis tools that are unable to handle defaulted destructors.
Fixes a crash whilst typechecking state machines that contained an event transition with a malformed event source.
Fixes a crash in the language server when the user’s cursor is over a malformed match expression.

1.2.5 (15/07/2022)¶

Bug fixes:

Fixes an issue that would cause the generated code to incorrectly call abort() when using match over an enum with exactly two cases, and where the match has precisely two cases, and where the value on the second clause is an empty block. For example:
```
function fn(x : Result<Nil, Nil>) : Nil = match (x) {
  .Error(_) => e,
  .Ok(_) => {},
}
```
would result in the generated code containing an abort() for the second branch, rather than an empty block.
Fixes an internal error when running verification on external types that include member functions that use nondet and are not marked with mut.
Fixes several issues that could cause the language server to crash when many events happend simultaneously.
Fixes an issue that would have caused the language server to report that a declaration could not be renamed sometimes, particularly if several renames were attempted in a row.
Fixed an issue that caused the coco_cpp_runtime.zip file to be empty.
Fixes an issue introduced in 1.2.2 that could have caused the generated code to not compile if a function parameter is not referenced, but is referenced by an external code expression.
Fixes an issue that caused Coco 1.2 to be incompatible with MacOS 10.15.
Fixes an issue with the generated code that would sometimes cause parameters to be passed by value rather than by reference. NonVerified<T> and T will now always be passed in the same way.
Fixes an issue that prevented the state dots inside the simulator from showing any data when clicked.
Fixes an issue where an incorrect URL would be used for automatic proxy detection.

1.2.4 (28/06/2022)¶

Bug fixes:

Fixes an issue with the Eclipse packaging that would cause the Coco Platform to be incompatible with Eclipse 22-06.
Fixes a case where the generated C++ code would not compile when using log with non-string-literals.
Fixes a warning when compiling the generated object-orientated C code due to non-static vtables.
Fixes an issue with the VScode plugin on Windows that would have caused most operations to fail with trying to get AST for unknown file.
Fixes a crash when generating C or C++ code from Coco models that refer to List<T>.

1.2.3 (20/06/2022)¶

Bug fixes:

Fixes a crash when generating C code from Coco models that compared types of the form NonVerified<T> for equality.
Fixes a crash when generating C and C++ code from Coco models that have use break in combination with match, under certain conditions.

1.2.2 (16/06/2022)¶

Bug fixes:

Fixes a case where the verification would fail with an array out-of-bounds error when using @unbounded under certain circumstances.
Fixes a case where the generated C and C++ code would not compile when using nested encapsulating components that have both construction parameters and external components.
Fixes a case where compiling the generated C++ code would result in warnings if -Wunused-parameter is used.
Fixes a case where compiling the generated C++ code would result in warnings if -Wnon-virtual-dtor is used.

1.2.1 (25/05/2022)¶

This is a small bugfix release to fix some packaging issues with the VSCode plugin. Users are advised to uninstall any pre-release versions of the plugin before installing the new plugin.

1.2.0 (25/05/2022)¶

This release contains no backwards-incompatible changes compared to 1.1, 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.

The release notes for the betas that led up to 1.2.0 can be found at 1.2 Pre-Releases. Relative to the final beta, this release contains the following changes:

The Coco VSCode plugin is now available from the VSCode Marketplace.
The architecture diagram in Eclipse will now intelligently select a default depth based on the complexity of the diagram.
Fixes an issue that would cause the generated C++ code to not compile when using @CPP.mapToType("unsigned int", ...).

New features:

Coco now has a new language server, which provides many more language features, and also has significantly improved performance on large projects (e.g. code completion on large files with many imports should now be instant, rather than taking seconds). The new features include:
- Semantically-aware renaming.
- Find all references can be used to find all places that a declaration is used.
- Module imports are now clickable in many more cases.
- Given a reference like X.Y, it is now possible to click on both X and Y in all cases.
- Components and ports show helpful information inline inside the editor, allowing for quick navigation to the components that provide/require other ports.
- Coco’s transform_subcommand are now available inside the editor and can be executed with a single click. Further, a new transformation has been added to fill in missing cases inside a match.
- In more advanced editors, such as VScode, Coco is able to provide semantically-guided syntax highlighting, which allows signal sends to be distinguished.
- Diagnostics will be provided more reliably in response to changes in files on disk.
- Stale error markers should no longer appear inside Eclipse.
The cloud verification service has been improved to increase throughput, and to reduce the chances of jobs being queued. Users should notice that jobs should always start extremely quickly, no matter how many other users are using the service, and that very large verification jobs (e.g. those with hundreds of models) will run many more jobs in parallel. In many cases, all verification jobs will be executed in parallel, unless there are dependencies between the jobs.

We now strongly recommend that all users enable the cloud verification as it will provide a better user experience than running verification locally.
This version includes a release of a language-only plugin for VSCode, which includes support for language intelligence inside VSCode, but does not include any support for verification or code generation etc. Download this plugin from the VSCode Marketplace.
Language:
- Components can now define constructors that take parameters and store them in non-verified instance variables. For example:
```
component C {
  val p : Provided<P>
  private val x : NonVerified<Int>
  init(x_ : Int) = {
    x = x_;
  }
  machine {
    p.fn() = x
  }
}
```
  Encapsulating components can then instantiate the component:
```
component Enc {
  val c : C
  init() = {
    c = C(2);
  }
}
```
  This should permit reusable components to be created more easily.
- SymmetricArray can be used to improve verification performance on components that have an array of provided ports, providing the component only stores a small number of identities.
- Ports can now inherit from multiple ports.
- Enums can now be mapped onto pre-existing enums in C or C++ using the new @mapToEnum attribute, allowing Coco pattern matching to be used even with enums defined outside of Coco. Further, Coco provides a @nonExhaustive attribute to ensure this is done safely.
- Coco can now refer to implementations of external components defined in code:
```
@runtime(.SingleThreaded)
external component LightBase {
  val p : Provided<Light>
}

@runtime(.SingleThreaded)
@CPP.mapToType("my_ns::LightImpl", .Value, .User("LightImpl.h"))
external component LightImpl : LightBase {
  val p : Provided<Light>
}
```
  This allows LightImpl to be used inside Coco within encapsulating components, which means that Coco will instantiate the external component implementation, rather than requiring it to be passed in via the Arguments struct in the generated code. This should make it much easier to instantiate and manage the Coco encapsulating components in the handwritten code. Further, external component implementations can even be declared as having constructors:
```
@runtime(.SingleThreaded)
@CPP.mapToType("my_ns::LightImpl", .Value, .User("LightImpl.h"))
external component LightImpl : LightBase {
  val p : Provided<Light>
  init(x : NonVerified<Int>) = {}
}
```
  This is supported by both the C++ generator and the object-orientated C generator.
- Coco’s auto-generated mocks can now be referred to from within Coco, allowing testing-specific encapsulating components to be constructed. For example:
```
import Testing

@runtime(.SingleThreaded)
external component External1 { ... }

@runtime(.SingleThreaded)
external component External2 { ... }

@runtime(.SingleThreaded)
component TestSystem {
  val mock : Testing.Mock<External1>
  val mock : Testing.StrictMock<External2>
  init() = { ... }
}
```
  The Testing module can only be imported from test code: see package.testSources.
- Coco now allows eventually assumptions to span multiple transitions. For example, the following port describes an interface that insists that following a call to start(), the finished() signal will eventually occur unless an emergencyHalt() function call occurs:
```
port Cancellable {
  function start() : Nil
  function emergencyHalt() : Nil
  outgoing signal finished()

  machine {
    static val kEventuallyFinishes : EventuallyAssumption

    state Idle {
      start() = setNextState(Running)
    }
    state Running {
      @satisfiesEventually(kEventuallyFinishes)
      emergencyHalt() = setNextState(Idle)

      @eventually(true, kEventuallyFinishes)
      spontaneous = {
        finished();
        setNextState(Idle);
      }
    }
  }
}
```
  Without the @satisfiesEventually(kEventuallyFinishes), a component that provided this port would be forced to emit the finished() signal after a call to emergencyHalt() due to the @eventually assumption.
- External components can now have provided and required ports. This can also be combined with @queue to generate skeleton C or C++ code that allows a component to be written by hand, but still to use the usual Coco constructs:
```
@queue(2)
external component C {
  val client : Provided<P>
  val req : Required<P>
}
```
  Warning
  
  Writing double-sided external components by hand is extremely difficult given there is no verification support. These should only be used by experienced users who have a specific need for such external components. Writing these components directly in Coco is strongly recommended.
Coco now has a second C generator that generates an object-orientated form of C. This is useful for large C projects that want to maximise code reuse, at the cost of using function pointers and a small amount of heap memory.

Warning

The new C generator is not yet fully stabilised.

Improvements:

Eclipse:
- Reachability counterexamples are now shown as a coloured overlay on the source code, like code coverage tools.
- The various views, such as the counterexample viewer and the architecture diagram, will now show a small warning in the corner when they are stale (i.e. when they do not reflect the most recent version of the file).
- The assertion tree now shows verification statistics as part of the tooltip, including the number of states, the number of transitions, how long verification took, and the amount of memory required.
- The structure viewer now highlights transitions that share the same implementation.
- The architecture diagram viewer has been improved to: improve performance on large diagrams; more intelligently show an initial depth on nested encapsulating components; improve the highlighting to highlight more relevant elements.
Frontend:
- Improved typechecking performance on very large projects, with runtimes and memory consumption reduced by up to 60%.
- Coco now has a profile system that allows stricter rules to be applied. For example, adding profiles = ["C++"] will cause Coco to reject some Coco programs that would result in invalid C++ being generated. The profile checks are under active development, and will improve significantly over the next few releases.
- Pretty-printing of types within error messages has been improved to ensure that the messages are not ambiguous.
- become is now checked by the typechecker, which will mean that errors that would previously have resulted in internal errors during verification will now be reported by the typechecker.
- Code completion on state machines now takes into account setAccess and setAllow calls.
Verification:
- The verification performance on large single-threaded models that contain many functions has been significantly improved. This reduces the runtime on some problems from tens of minutes to one or two minutes.
- The command-line verification progress output has been improved to provide an animated interface that displays which jobs are running, and also summaries of how many jobs are running in each stage.
- Added an option to the command line to limit the number of verification jobs run in parallel.
- Added the verification time to the JUnit XML output for verification results.
- Coco now includes an experimental JSON output format for verification results.
Releases:
- The Linux release binaries are now compatible with RHEL6. Due to the age of RHEL 6, this is not guaranteed and is only offered on a best-effort basis.
- The Linux release binaries are now also available for 64-bit ARM cpus (ARMV8-A or later).
- The downloadable archives of CLI tools now correctly set permissions when extracted, meaning that the files should be immediately executable.
- The Mac release binaries are now codesigned and notarised, meaning that the tools should be executable immediately after download without right-clicking.
C++ Generator:
- The C++ generator is now able to generate code for functions that are generic over the Iterable trait.
- Immutable variables in Coco now create immutable variables in C and C++.
- The JSON code index now includes an entry describing the mutability of a parameter’s type.
- operator[] can now be referenced using @CPP.binaryOperator.
- A new option generator.cpp.illegalBehaviour has been added that allows customisation of how Coco handles illegal behaviour in the generated code, providing the single-threaded runtime is used.
- A new option generator.cpp.loggingHeaderFile has been added that allows a custom header file to be specified that overrides the default Coco logging macros to use user-defined logging macros instead.
- A new option generator.cpp.useHierarchicalNames has been added that allows users to choose whether the logging code uses nested names like x.y or flat names like y.
- When generating code, if a file has not been changed then the original access time will be preserved.
- Coco’s generated mocks now include send_ helper functions to easily send signals, including via the GMock Invoke action.
- Cast is now fully supported when generating C++, and will correctly generate C++ code corresponding to user-defined cast instances.
Simple C Generator:
- The generated C code is now placed into the files containing each component, rather than concentrated into the file containing the encapsulating component.
- Added an option to allow C header files to be generated into extern C blocks.
- Added support for arrays of components and arrays of required ports to the C generator.
- The C generator now supports unique.
- Added an option to the C generator to create typedefs for all Coco-generated structs and enums.
- bool can now be overriden when generating C code.

Bug fixes:

Fixes an issue that would cause Eclipse on Windows to crash with errors about the number of handles.
Fixes a crash when verifying functions that contained a nondet where a clause had a guard that referenced a variable of type &T that was an argument of the function.
Fixes an issue with --error-limit and --warning-limit that would result in notes that were attached to suppressed errors or warnings still being emitted.
Fixes a crash when viewing architecture diagrams of encapsulating components that contained arrays of encapsulating components.
Fixes several cases where clicking on the architecture diagram would not navigate to the corresponding code.
Fixes a case where static vals would be initialised to incorrect values if one static val referenced another static val in the initialiser.
Fixes a bug that would prevent the generated code from being compiled if a struct contains no fields.
Fixes a case where the generated code was needlessly verbose when using ?.
Fixes a bug that would cause type aliases to not be emitted in the generated code.
Fixes a case where the generated GMock mocks would not compile when using Result.
Fixes a crash when generating architecture diagram for encapsulating components with arrays of components.
Fixes a crash when using setShared in a specific combination with port inheritance.
Fixes a case where a slot could be compared for equality with another slot even if its contents were invalid.
Fixes an internal error that was raised when using port inheritance on ports that include only functions.
Fixes a crash when parsing files that accidentally declare provided or required ports inside state machines.
Fixes an issue that caused -e to be parsed incorrectly when there was no space between - and e.
Fixes several issues when using unused() or timers in single-threaded models that also use setShared or have multiple provided ports. These issues would have led to false counterexamples being generated.
Fixes an issue that could have prevented single-threaded state machines from terminating cleanly when running the generated code if the state machine could receive a signal synchronously in an unused() transition.
Fixes a case where Coco incorrectly identified duplicate typedefs as being disallowed in C++, thereby blocking the generation of C++ code.
Fixes a crash when @CPP.mapToValue was used on a member function of an external type.
Fixes a case where Coco would not check an import is from a direct dependency listed in the Coco.toml file.
Fixes a crash that occurred when trying to render the architecture diagram for very large encapsulating components.
Fixes several issues with the pretty-printer that would cause the support-bundle command to generate incorrect Coco files.
Fixes a bug that would cause code completion for arrays of provided or required ports to suggest invalid Coco code.
Fixes a bug that would prevent encapsulating components from being constructed where a provided port of the encapsulating component connects to a provided port of an internal component that is also required by another component.
Fixes a bug that caused an internal error when verifying components that used two ports that each contained a state machine defining a static val of the same name.
Fixes a case where the generated C++ code would not be compilable when using arrays of components that have constructors. This includes both arrays of components with user-defined constructors in Coco, and arrays of encapsulating components that contain external components.
Fixes the generated C++ code to always default the name, as per the documentation.
Fixes a bug that would cause the generated C code to not compile when using multi-dimensional arrays.
Fixes several bugs with complex patterns in match expressions that would cause internal errors during verification.
Fixes an internal error when verifying models that include enums E with member functions that have parameters that also include type E.
Fixes a case where side-effect would incorrectly be allowed on enum case patterns with if conditions.
Fixes a crash that could occur when using cloud verification where Eclipse is open for more than 24 hours.

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:

Single-threaded mocks now include a gMock action to send coco_drain_queue() to all connected clients.
coco::SingleThreadedGMockHelper can now be used as a coco::SingleThreadedTimerExecutor, allowing easy-testing of single-threaded compponents that use timers.

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.