1.3 Pre-Releases¶

1.3.0-beta.11 (24/04/2023)¶

Breaking changes:

The encapsulating component validator has been modified to reject some single-threaded architectures that use multi-client architectures in a way that is potentially unsafe at runtime. Specifically, if a single-threaded component C has a multi-client required port r that is connected to a provided port p, then Coco now ensures that p is not directly used by any other required port of C.

If this change causes a problem, then the suggested refactoring would be to split the provided port into multiple provided ports.
The new Vector modules have been refactored to use UInt instead of Int, and also use Bounded<0, maxSize - 1, UInt> rather that Bounded<0, maxSize, UInt> where appropriate. This should also prevent some cases where the generated C++ code would not compile when compiled with warnings.
When using the language standard 1.1, ports are no longer allowed to define the names ambiguous, call, drainQueue, processQueue, send, timer, or unused.
The Coco EMF metamodel has been altered to reuse more nodes between await clauses and transitions. The main change is that there are no longer separate Transition subclasses, and instead there is a single Transition class that has an event property.

New features:

There is now a JSON output format for the diagnostics raised by coco, complementing the existing XML-based one. See Schemas for further details on the format. To use this, run coco with --diagnostic-format=json.
coco can now output the cognitive complexity of all functions defined in a package by using the metadata --ast command.
There is now an additional Coco Tidy check called ReadabilityOfferIf that can identify cases where an offer is being used but a simple if-then-else would suffice.

Improvements:

@ignoreWarning(.DeadState) now behaves more appropriately in the case of state machine inheritance, and un-extended states will now inherit the warnings from the base state.
The generated C code will now comply with -Wstrict-prototypes.
Coco now generates a warning when there are unused provided ports of components. These warnings can be suppressed using @ignoreWarning(.Unused) on the instance of the component that has unused ports.
There is now a setting package.generateCode that can be used to prevent code generation from being directly invoked on a package. This can be used for utility packages that should never have their code directly generated.

Bug fixes:

Fixed an issue that meant that @ignoreWarning(.DeadState) had no effect when applied to a state machine.
Fixed some missing const annotations in the C++ runtime header.
Fixes an issue that could cause user-defined attributes to be dropped on optional nodes.
Fixes a case where single-threaded multi-client verification could fail with a counterexample that should not be possible.
Fixes a case where the generated code would not compile when using arrays of external implementation components.
Fixes a case where purge() would not work correctly during verification when combined with port inheritance.
Fix a crash when opening EMF-produced ASTs where an attribute has the wrong number of arguments

1.3.0-beta.10 (14/03/2023)¶

Improvements:

tool.requiredVersion now allows pre-releases to match inequalities like >= 1.2.18.
--stats-json can be used to output simple statistics about the resources an execution of the command-line tool took.
The command-line verification can now output json results and junit results in parallel to specified files.

Bug fixes:

Fixes an issue that would prevent non-verified types with @mustUse from being used as arguments to functions or signals in a port.
Fix an internal error when verifying models that use Slot<T> with a T that contains member functions but no fields.
Fix a crash when verifying state machines that consume too much data. A clean readable error is now reported.
Fix a crash when typechecking an await that is syntactically invalid.
Fix several crashes when generating code fails due to a filesystem error.
Fixes an issue that would cause the inlay hints to flick on and off in VScode.
Fix a crash when hovering over certain inlay hints in VScode.
Fix a crash when performing renames.
Fix a crash when performing code completion on struct literals.
Fix a crash when performing code completion on arrays of ports.
Fix a crash when performing code completion on generic types that include incorrect literal types.
Fixes an issue that would cause the architecture diagram’s zoom level to be miscalculated.

1.3.0-beta.9 (01/03/2023)¶

Bug fixes:

Fix a crash when using @mapToEnum on an enum that is nested inside a port.

1.3.0-beta.8 (28/02/2023)¶

Improvements:

Counterexamples now include more readable event names for spontaneous, nondet, offer, timer and other internal events. By default, they try and use the transition name and any value given by @represents. If these are not present, then an auto-generated string based on the syntax will be shown.
Coco now generates a sentinel function when @mapToEnum is used without @nonExhaustive that will cause the generated code to not compile if the Coco version of the enum is missing a case that is present in the C++ enum.
- Note this depends on compiler-specific flags. For GCC 4.4 this only works if the user has manually set -Wswitch and -Werror. For more modern compilers, the generated code automatically sets these flags as required.
The code index now includes whether a module is a test module, or a regular module.
When renaming Coco declarations, Eclipse will now default the name to the original name.
Add a warning if a variable is referenced but its value is not used.

Bug fixes:

Fix an issue where the generated code would not compile with pre-C++11 compilers under certain conditions if @mapToValue, @mapToEnum, or @mapToType was used with a globally-qualified name (e.g. ::X).
Fixes a case where the verification would not fail when unsubscribe was used in conjunction with await.
Fixes a case where unreferenced member functions inside enums that are marked with @mapToEnum would not be generated.
Fixes a crash when typechecking enums that had incorrect attributes applied.
Fixes an issue that would prevent the generated C++ code from being compiled when using clang with older versions of libstdc++.
Fixes some cases where the transition names were allowed to clash with normal Coco names.

1.3.0-beta.7 (17/02/2023)¶

Improvements:

Coco now includes a new builtin module, Vector, that includes four new builtin types:
- BoundedVector<T, val maxSize : Int>: models a vector whose contents are unknown during verification, but where the size is known as a Bounded<0, maxSize>.
- NonVerifiedVector<T>: models a vector whose size and contents are not known during verification.
- UnboundedVector<T>: models a vector whose contents are unknown during verification, but where the size is known as an Int.
- VerifiedVector<T, val maxSize : Int>: models a vector whose contents and size are known during verification.
All of these vectors map to C++’s vector type.
Transition labels can be applied to nondet and offer clauses.
Awaits with stop conditions can now be used as expressions providing the expression is of type Nil.

Bug fixes:

Fixes a case where inlay hints could be doubled if an implicit cast was used.
Fixes a case where @mustUse was not checked on unused parameters.
Fixes an internal error when verifying models that contain await where one of the branches calls abort().
Fixes several cases where the ecore editor would not expand await events fully.
Fixes a case where sealed encapsulating components could not be included in other encapsulating components without incorrect errors about the instance being unconnected.
Fixes a bug that prevented mocks from being assigned to external component fields.
Fixes a case where the generated code for external functions on enums that did not use @mapToValue was incorrect.
Fixes a crash when loading certain malformed files in the language server.
Fixes the semantically-aware rename calculation when renaming module-level variables.
Fixes a crash when a file consists only of an unused import.

1.3.0-beta.6 (09/02/2023)¶

Improvements:

Name-based refactorings suggested by Coco Tidy can now be refactored with one-click inside Eclipse.

Bug fixes:

Fixes a bug that could cause the verification to fail with incorrect loop counterexamples when there are large numbers of @eventually properties.
Fixes a case where subprocesses spawned by coco outlive coco itself.
Fixes an issue with presenting await clauses in the reflective ecore viewer.

1.3.0-beta.5 (03/02/2023)¶

New features:

Code completion now works inside Coco.toml files and suggests additional settings, and values of enums where appropriate.
Links to declarations inside builtin modules (like Base.coco and CPP.coco) are now fully navigable inside editors, allowing Coco’s primitives to be inspected.
Coco now incorporates a code linting feature called Coco Tidy that provides suggestions on how to improve the readability of your Coco code. There are several checks available at the moment:
- ReadabilityBoolLikeEnum: flags enums that appear to be equivlent to Bool.
- ReadabilityCognitiveComplexity: checks whether any function exceeds the specified cognitive complexity threshold indicating that the function should be refactored into multiple blocks.
- ReadabilityElseAfterControlFlow: checks whether an else is used after a control flow statement that guarantees the else is unnecessary. For example, an else clause following a then clause with a return at the end of it will cause this warning to be raised:
```
if (...) {
  return 0;
} else {
  ...
}
```
- ReadabilityNaming: checks that all names conform to a specified style (e.g. camelCase or similar). Different styles can be specified for different sorts of names; to see the various names supported try using code completion on the [tidy.ReadabilityNaming] section of the Coco.toml file.
- ReadabilityPortOfferNondet: when an offer is used where a nondet is equivalent, the tool suggests using nondet in order to improve readability.
The checks that are enabled can be specified in the Coco.toml file as follows:
```
[tidy]
enabled = ["*", "-ReadabilityBoolLikeEnum"]
```
Each clause in enabled either enables or disables (by using -) a check. For example, -Readability would disable all readability-related checks.

Improvements:

Various improvements have been made to the generated C++ code with the aim of reducing the size of the compiled code, particularly when compiling components which could receive many different signals.
Further documentation has been added on await.
It is now possible to disable warnings about unused imports via the language.disabledWarnings setting.

Bug fixes:

Fixes an issue that would cause diagnostics inside Eclipse to not be removed when editing the file outside of Eclipse (e.g. inside another editor or when using version control tools).
Fixes an issue when using authenticated proxies.
Fix a crash when deserialising EMF modules.

1.3.0-beta.4 (23/01/2023)¶

Breaking changes:

The guard on await clauses has been moved from before the clause to after the clause to allow the guard to inspect the values of the parameters:
```
await {
  r.sig(x) if (x == 2) => { ... },
}
```

New features:

Encapsulating components can now instantiate inner encapsulating components and specify which external implementation components should be used. For example, the following shows how to instantiate an existing encapsulating component and use a mock at runtime:

@runtime(.MultiThreaded)
component System {
  val ext : ExternalComponent
  ...
}

@runtime(.MultiThreaded)
component TestSystem {
  val extMock : Testing.Mock<ExternalComponent>
  val inner : System
  init() = {
    inner.ext = extMock;
  }
}

Static functions can now be defined on enums, external types, and structs, and can be either external or regular Coco functions. Static functions can be used to define convenient constructors on Coco-defined types. For example, consider the following:
```
struct S {
  var x : Bounded<0, 5>
  var y : Int

  static function create(x : Int) : S = S{x = .First, y = x}
}
```
Given the above, the static function can be invoked via S.create(5).
External functions can now be defined on enums and structs, and functions can be defined on external types. This allows helper functions that enhance external types to be defined in Coco, but on a non-Coco defined type.

Improvements:

Coco’s language server now supports workspace-wide symbols searches in both VScode and Eclipse.
Coco now provides a warning when an import is unnecessary, along with an automated fixit.
Array event sources in components can now be parameterised by any type T providing Integer<T>.
Improve compatibility with new Eclipse versions which was causing Eclipse to generate a warning about the encoding not being specified.
@C.requireStatement and @CPP.requireStatement have been added which allow functions that return Nil to be called as a statement, rather than as an expression. This can be useful if the function is implemented by a C macro that results in a statement, rather than an expression.
Attributes can now be applied to an entire module, rather than just one declaration.
@C.defaultHeaders and @CPP.defaultHeaders have been added and can be used to specify the headers that all external types and functions should inherit within a given module. For example:
```
@CPP.defaultHeaders(.User("time.h"))
module

@CPP.mapToType("S")
external type S

@CPP.mapToType("T")
external type T
```
The above is equivalent to adding the .User("time.h") header to both S and T.
Coco is now able to load larger projects around 30% faster thanks to performance improvements to Coco’s typechecking.
Coco beta releases are now published on the VScode Marketplace. Note that although the release numbers are different due to limitations on the VScode Marketplace, the underlying releases are the same as the corresponding Coco Eclipse releases.
Official docker containers are now available for Coco. These containers are available based on either a stripped-down container or based on Ubuntu 22.04, and are available for all architectures that Coco supports. Specific Coco releases can be downloaded by using the corresponding tag:
```
$ docker run docker.cocotec.io/coco:1.2.16 -version
$ docker run docker.cocotec.io/coco:1.2.16-ubuntu22.10 -version
```
Alternatively the latest stable version can be accessed via the latest tag:
```
$ docker run docker.cocotec.io/coco:latest -version
$ docker run docker.cocotec.io/coco:latest-ubuntu22.10 -version
```
Lastly, the testing tag can be used to run the latest beta release:
```
$ docker run docker.cocotec.io/coco:testing -version
$ docker run docker.cocotec.io/coco:testing-ubuntu22.10 -version
```
Specialisations can now be consistently specified next to the type; e.g. Result<Bool, Nil>.Ok is now consistently accepted. Previously, the specialisation had to sometimes be provided at the end, e.g. Result.Ok<Bool, Nil>.
The VScode syntax highlighter is much improved and is able to elegantly highlight most of Coco.
The required version of Coco can now be specified in the Coco.toml file:
```
[tool]
requiredVersion = ">= 1.2.0"
```
See tool.requiredVersion for further details.
The counterexample viewer has been enhanced to allow specific variables to be selected and then traced through counterexamples.
Nested encapsulating components can now be navigated conveniently by double-clicking on sub-encapsulating components, which will zoom in on an expanded view of that specific sub-encapsulating component. Breadcrumbs are provided to allow easy returns to higher levels.
Diagnostics that are caused by the wrong sort of type being used (e.g. an enum where a port was expected) are now clearer.
All match clauses can have a guard, rather than just enum case and state patterns.
The verification cache now ignores irrelevant settings from the Coco.toml file, meaning that results should more often be cached.
The exit code of the coco program has been improved to distinguish between expected errors (e.g. the typechecker failed), and fatal errors (e.g. could not connect to the verification server).
Long await clauses are now formatted more elegantly.
Transitions can now be given names:
```
MyTransition: p.fn() = { ... }
```
The remote verification backend now distinguishes between out-of-memory and timeout errors.

Bug fixes:

Fixes a case where Coco would incorrectly allow the same module to be imported multiple times.
Fixes an issued that caused disabledWarnings to have no effect.
Fix an issue that caused await to process the first item in the queue too early, meaning that the verification did not consider one specific interleaving.
Fix a case where await clauses would incorrectly be marked as unreachable.
Fix a crash when generating code using await on components that contained arrays of ports.
Fixes the EMF serialisation of await.
Fix a case where Eclipse fails to show the code lenses for a port or component.
Fix a crash when running semantic highlighting on complex generics.
Fix a case where the parser would not parse calls on struct literals (e.g. S{x = 2}.f()).
Fix a crash when verifying models that convert NonVerified<Int> to Duration.
Improves the behaviour of the tool when the verification cache is unresponsive.
Fixes a case where the renamer would not rename types that were referred to inside cast or default expressions.
Fixes a case where using the detail slider in Eclipse would not kill the existing rendering process if it has not yet completed.
Fix a crash when generating C code that used complex static vals.
Fixes the C code generator when accessing multi-dimensional arrays.
Fixes an issue that would lead to code lenses missing in Eclipse after the first load.
Fixes a bug that caused cached verification statistics to not be visible inside Eclipse.
Fixes a case where the typechecker would reject calls with a conflicting references error even though there was no conflict.

Additionally, this release includes all bug fixes contained in Coco versions 1.2.10 to 1.2.17.

1.3.0-beta.3 (30/09/2022)¶

New features:

Components are now able to block function calls received over the provided port until a signal arrives from a required port. For example, the following Coco snippet will cause the calling thread to be blocked until either a finish signal is received, or until a timer elapses:
```
client.fn() = {
  req.start();
  return await {
    req.finish(result) => .Ok(result),
    after(seconds(1)) => .Error(.Timeout),
  };
}
```
await is supported in both runtimes (although single-threaded components cannot block and thus can only handle signals that are received synchronously), and is also supported by all code generation languages.

See await for further details, including details for how to block until the queue is empty (via empty event), or how to defer handling signals to the main state machine (via inherit).

Use of await requires standard = "1.1" in the Coco.toml file. This standard is only a minor change from 1 and the only change is that there are several new keywords. Upgrading to 1.1 will therefore only require variables that clash with the new keywords to be renamed. The new keywords are abstract, await, inherit, trace and verify. This list is subject to change until the final release of 1.3.

Warning

This feature is in beta, and even the syntax may change before the final release of 1.3.
CPP.mapToMember now has an optional second argument that allows the choice of -> or . to be customised. For example, @CPP.mapToMember("reset", .Arrow) would cause the generated code to map all calls to reset to be of the form obj->reset().

Improvements:

Nested encapsulating components can now be easily navigated in the architecture diagram; double-clicking on a node in the diagram will show the diagram for the sub-encapsulating component, and breadcrumbs allow easy navigation back out of the inner diagram.
The Bounded type that is automatically deduced for arrays of ports is now simplified to no longer include -1 symbolically, providing it is possible to compute the argument.
Improved the formatter to improve handling of long nondet expressions where the trailing comma has not been specified.
Improved the typechecker’s handling of break and continue inside blocks to provide better error messages in case of malformed Coco programs.

Bug fixes:

match is now correctly prevented from using a value of type Slot<T>. This would have led to an internal error during verification.
Fixes an issue when clicking on the Provided/Required by x components messages inside Eclipse that would have resulted in the incorrect results being displayed.

1.3.0-beta.2 (12/09/2022)¶

New features:

Coco imports can now be explicitly scoped by package, e.g. import pkg:Module. When used in combination with the new setting, language.packageScopedImports, this means that different Coco packages can now define modules that have the same name without causing errors.

Improvements:

When generating C or C++ code, the output directory for header and implementation files can now be set separately using the generator.cpp.headerOutputDirectory, generator.cpp.implementationOutputDirectory, generator.cpp.testHeaderOutputDirectory, and generator.cpp.testImplementationOutputDirectory settings.
When generating C or C++ code, a prefix can now be applied to the filename of each file using the generator.cpp.headerFilePrefix and generator.cpp.implementationFilePrefix settings.
The command line tool can now execute commands on only a subset of packages in a workspace using the coco --packages option, which accepts a glob-like pattern (e.g. A* means any package starting with A).
Coco’s remote verification is now enabled by default.
Proxies are now automatically detected on MacOS.
Coco’s file system watcher, which reloads projects whenever files change, has been improved:
- Performance on large directory trees where only some directories are relevant to Coco has been significantly improved.
- Watching on Linux should be more reliable and use less memory.

Bug fixes:

Fix a crash when loading a workspace that contains a package with no files.
Fix a crash when loading a package that is in a workspace that is invalid.
Fixes a crash when Coco finds a package with an enclosing workspace that does not list it as a member.
Fixes an issue that would prevent loading files on network shares on windows.
Fix a crash when rendering architecture diagrams that use external implementation components.
Fixes an issue when loading workspaces where several packages define a module with the same name.
Fixes an issue that would prevent the Coco Eclipse plugin from functioning correctly when Eclipse proxy settings are set.
Fixes an issue that would prevent offline licenses from working with the cloud verification service, if connectivity is later available.

1.3.0-beta.1 (23/08/2022)¶

New features:

Coco now supports workspaces, which are folders with collections of packages, potentially also with defaulted settings. For example, suppose a folder contains a Coco.toml file with the following contents:
```
[workspace]
members = [
  "A",
  "B",
]

[language]
standard = "1"
```
This will cause Coco to automatically load the Coco packages that are in the A and B subfolders and, further, will apply the settings inside the workspace to the packages inside A and B as well.
Apple Silicon is now a fully supported platform, including inside Eclipse, the CLI tooling, and VScode.

Improvements:

External types can now have member functions without having data members.
The command-line tool now only draws encapsulating components, rather than all components.
Added a compile-time version check for the C runtime.
Improved the error messages when generating code that refers to static vals that do not have a mapToValue annotation.
The support-bundle command now compresses its output.
Coco now loads TLS certificates from the system certificate store on Windows.
Added further documentation on guards for enum case patterns and how mapToValue should be used on external constants.

Bug fixes:

Fixes several cases where the verification would incorrectly fail with a deadlock whilst verifying complex multi-client systems.
Fixes a crash when verifying models that use struct literals as top-level vals.
Fixes an incorrect warning about variables not being used when embedding assignments inside other expressions.
Fixes a case where the generated C++ code would not compile when matching the value of a state machine variable that has a non-zero default value.
Fixes a case where the generated C++ code would not compile when using static vals on structs and ports.
Fixes a case where casts were incorrectly parsed with a too-high precedence.
Fixes a case where the code reachability annotations inside Eclipse would not be dismissed.
Fixes a case where the structure diagram incorrectly handled inherited signals.
Fixes several cases where the pretty printer produces invalid Coco code.
Fixes a crash when a package depends on itself.
Fix a crash when verifying components that have private val fields that are of an external type that has member functions.
Fixes a case where the typechecker incorrectly allowed a nested port to contain a state machine.