Release Notes¶
1.5.0 (24/06/2025)¶
Breaking changes:
- Popili for Linux now requires at least glibc 2.28 to run.
- Popili for MacOS no longer supports Intel CPUs.
- When using the mixed runtime with a single-threaded component with a multi-threaded required port that has unbounded
spontaneous transitions, you must now use an
Unbounded
queue; e.g. replace@queue(2)
with@queue(.Unbounded(2))
. An automated fixit is available for this.
Highlights:
The Coco Platform is now known as Popili, and all of our tools have been updated to reflect this. This includes the command-line tool, which is now invoked as
popili
instead ofcoco
. If you are using the automatic downloader added in 1.4, then no changes are required: this will transparently use the correct name based on the version. The Eclipse and VSCode plugins will auto-update to the new names as part of the usual update processes with no user intervention required.The Popili VSCode plugin has been significantly enhanced and it is now able to be used as a full development environment for Coco. The plugin includes:
- Support for running the verification and debugging counterexamples:
- Popili for VSCode includes a verification tree that shows all Coco models in your package in a similar way to Eclipse, but using the native VSCode controls and UI paradigms.
- Behavioural counterexamples are presented as a sequence diagram but are integrated with VSCode’s native debugger.
- Reachability counterexamples are presented via a separate interface and show as an overlay on the state diagram, an overlay on the structure diagram, and also as inline annotations on the editor showing which lines are reachable or unreachable.
- Verification statistics are also available as a table, which allows for a quick overview of which models are taking the longest to verify.
- The verification has been deeply integrated into VSCode, and statistics and verification results are now shown as contextual information in the editor (e.g. in tooltips) in relevant places.
- Counterexamples automatically update when the verification is re-executed.
- The simulator. This uses the same debugger and sequence diagram viewer as the counterexamples. Compared to Eclipse, the VSCode simulator is significantly easier to drive via the keyboard.
- Support for generating code, either via a dedicated command in VSCode’s command palette, or via a button on the assertions tree (like Eclipse).
- Support for helping users get started, including:
- A welcome page that integrates with VSCode’s welcome pages, helping new users get a license and open their first Coco project with Popili.
- A command to install the Coco examples.
- A command to create a new project in a given folder.
- A command to create a support bundle when users run into problems.
- Vastly improved licensing support:
- The login process will no longer happen on its own; instead you can click login at the point you want to start authenticating.
- The license status is clearly shown in the Popili status icon in the icon bar, and various options are provided to login.
- Popili for VSCode now supports offline licenses.
- Support for floating licenses has been improved, as users are now able to choose when to activate Popili and thus attempt to acquire the floating license.
- Improved integration between VSCode and Popili features:
- The architecture and state diagrams now automatically restore when VSCode is re-opened, and also update promptly after edits are completed, rather than just on save.
- Improved support for VSCode’s remote feature, where the language server runs on a remote connection.
- The counterexample diagrams are themed using VSCode’s native themes.
- The architecture and state diagrams now use controls that are natively styled by VSCode.
- Support for running the verification and debugging counterexamples:
Coco Language:
- Several restrictions on the mixed runtime have been lifted, including:
- Signals can now be emitted from all spontaneous transitions, not just unbounded ones.
- Signals can be sent synchronously from function calls, though they will be received asynchronously.
- Arrays of required ports can be marked with
@runtime(.MultiThreaded)
. - Single-threaded encapsulating components can now have multi-threaded required ports, allowing multiple levels of encapsulation.
purge
,subscribe
andunsubscribe
are fully supported on multi-threaded required ports.
- Several restrictions on the mixed runtime have been lifted, including:
The Coco language now incorporates a
Display
trait that is intended to allow users to define methods for converting types into human-readable strings (unlikeLog
, which is intended for both human and machine-readable representations). For example:In the Coco 2024 language standard,
Display
is the default trait used in format strings (i.e.$"Hello {name}"
would useDisplay
, notLog
).popili
now supports external authentication providers, enabling easier integration into CI environments that provide secure credentials, such as Buildkite, Github Actions or other cloud providers who use OIDC. Contact support@cocotec.io to set this up for your organisation.Coco now has full support for 8, 16 and 32 bit signed and unsigned integers;
Base.coco
now containsInt8
,UInt8
etc.
Improvements:
Coco Language:
There is a new Coco language standard available, called
2024
. This differs from1.2
as follows:Format strings now use the
Display
trait instead of theLog
trait by default. For example:$"Hello {name}"
would convert
name
to a String by invoking theDisplay
trait instead of theLog
trait.When value logging is enabled (as added in Popili 1.4), the generated code now logs signal sends. This can be disabled by setting the
generator.cpp.logSendSignals
option tofalse
.For the C and C++ generators, the runtime will not be header-only by default.
For the C, C# and C++ generators, signal sends will be logged by default.
Functions declared as
@noSideEffects
on Coco ports will now be mapped to const member functions in C++.
Going forward, Coco language standards will use year-based versions instead of semantic versions to help disambiguate tool versions from language versions.
See migrating to Coco 2024 for advice on upgrading.
The
@queue
attribute now accepts an integer literal of any type.@ignoreWarning(.Unused)
can now be used on encapsulating components to suppress warnings about unconnected provided ports if this is expected.Literal expressions are now bounds checked inside struct literals.
Coco now includes specific syntax for ranges.
0..5
is equivalent torange(0, 5)
(i.e. up-to but not including5
), whilst0..=5
is equivalent toclosedRange(0, 5)
(i.e. up-to and including5
).Type aliases can be declared inside external types and structs.
type(e)
can now be used as a type to extract the type of an expressione
.Transitions that are marked as illegal must now use
_
as their parameter name.The builtin Coco
Base
module is no longer treated like an unqualified import, allowing users to define their own types that override the types inBase
. This will help ensure that as Coco’s standard library is enlarged, user code will not break even if it uses the same names.Formatter
now contains overloads ofwriteInt
for non-verified types.The
Vector2
vectors types now have aSize
member type. For example when combined with thetype
operator, this allows the following code to be written:var x : Vector2.BoundedVector<NonVerified<Int>, 5>; var pos : type(x).Size = x.size();
The
Duration
-construction functions, includingseconds
etc can now be used at the module-level as part of constants.
Language Server (Eclipse and VSCode):
- The imported module contains errors error is now only created for files that are open, making the problems view summary much more useful in VSCode and Eclipse.
- Diagnostics (e.g. warnings and errors) now include notes even if those notes are in different files.
- Improves the fixits for unused parameters to suggest replacing the name with
_
. - Improves the formatting of struct literals nested inside attributes.
- Wildcards are now correctly used when performing code completion on monitors.
- Coco tidy is now able to enforce naming standards on transition names and labels.
- Code completion hints on encapsulating components have been improved, particularly when using external implementation components.
Verification:
- Improves verification cache hit rate when only comments are changed.
- Models that contain stack overflows due to, for instance, unbounded recursion, are now caught by the verification and helpful counterexamples are now produced.
- Single-threaded multi-client required ports are now less concurrent on startup, matching the runtime behaviour.
Log Replay:
- Line numbers are now displaying counterexamples from log files.
- Adds an option to suppress the error that is normally raised when no events match a monitor.
- Adds support for using the
VerifiedVector
type as a parameter type when replaying logs. - Adds an option to specify the maximum counterexample length, and improves the counterexample presentation so that it is clearer when the limit has been reached.
popili replay
now permits multiple log files to be replayed at once.- The log replay now allows parameters or return values that are not used by the monitor to be omitted from the logs.
Tooling:
- Attributes are now included as part of the output of popili metadata. This can be used to build tools that generate additional code based on the values of the attributes.
tool.selectedVersion
can now omit the patch version.- A warning is now generated when if
tooling.selectedVersion
is set to an unsupported version of Popili. - The .NET API now provides explicit IDisposable implementions rather than just relying on finalizers.
- The Popili Java API is now available as a Maven-compatible artifact.
- Added a generate command to the
popili
command-line tool that will generate code for the language set ingenerator.defaultLanguage
. This is a language-neutral variant of thegenerate-cpp
subcommand. - The command-line tool now allows verification warnings to be treated as errors or not. This is particularly helpful when using the JUnit output option.
VSCode:
- Improves the code completion behaviour to avoid problems where the editor would automatically select completion items in an unhelpful way.
- Improves the highlighting of functions that implement operators, such as
equals
. - The language identifier for Coco has been changed to
coco
to match other languages. - The various diagrams can now be saved in bitmap formats, in addition to SVGs.
- Diagrams can now be copied directly to the clipboard.
- Diagrams now auto-update without saving.
- VSCode will now prompt to restart Popili if
tool.selectedVersion
is modified. - Popili’s preferences can now be configured via VSCode’s settings UI.
- Improves the opening of diagrams to more consistently not open the diagrams over the top of editors.
- Improves the behaviour of the state diagram and architecture diagrams when a license is lost.
- VSCode now displays the Device Code more prominently during the login process.
- Deprecated or unused declarations now have more distinct styling when using VSCode.
Code Generation:
- All: the builtin stream logger implementations now support logging timestamps in the local timezone, instead of UTC.
- C++ Generator:
coco::variant
andcoco::optional
now use exceptions like their STL counterparts.- The
stream_logger.h
header file has been split into two to enable it to be used on embedded platforms that do not support iostream or mutexes. - The runtime header has now been split into a header and source file. This can be disabled by setting
generator.cpp.headerOnlyRuntime
totrue
. This is enabled whenlanguage.standard
is set to2024
, and should result in faster compilation times when used. - The generator now supports
@mapToTraitInstance
, allowing trait instances to be mapped onto pre-existing partial specializations of a trait struct. - Adds a
@mapToConstructor
attribute that can be used to indicate a function maps onto a constructor in C++. - Whether the generated C++ mocks are header-only or not can be controlled via the
generator.cpp.headerOnlyMocks
setting. This defaults to true, but can be set to false in which case a .cc file will be generated as well. Testing
now containsNiceMock
which will map to GMock’s :icpp:`testing::NiceMock` class in the generated code.- Types that are not defaultable in C++ code can now be used as the types of state machine variables.
- Adds a new option
generator.cpp.shortenIncludes
that will cause the C++ generator to shorten includes to files in the same directory.
- C# Generator:
- C#: Adds an option to create C# namespaces for Coco folders.
- C#: External components now have a virtual
Dispose
method that can be overridden to add custom dispose logic. - C#: add support for
generator.csharp.fileHeader
to allow a static file header to be prepended to a file. - Mocks
- C Generator:
- Adds support for the
Signal
datatype. - Popili will now auto-generate warning supressions for unused parameters in C when it has to generate a name in order to comply with the C standard.
- The runtime header has now been split into a header and source file. This can be disabled by setting
generator.c.headerOnlyRuntime
totrue
. This is enabled whenlanguage.standard
is set to2024
, and should result in faster compilation times when used. - The runtime headers are now more compatible with embedded environments that are not strictly POSIX compliant.
- Adds a new option
generator.c.shortenIncludes
that will cause the C++ generator to shorten includes to files in the same directory.
- Adds support for the
Bug fixes:
- Coco Language:
- Fixes an issue with
await(true)
that would cause the out parameter analysis to be incorrect. - Fixes a crash when typechecking generic struct literals where type inference fails.
- Fixes a language server crash when requesting code completion on a declaration name.
- Code completion now respects
setAllow
filters on monitors. - Improve code completion behaviour when typing
:
in the editor. - Fixes obfuscation of type casts, such as
e as T
when generating support bundles. - Fixes a crash when incorrectly instantiating generic types with modules.
- Fixes a case where some side-effects inside arguments marked with
@noSideEffects
would not be rejected. - Fixes an issue with the code completion on signals which was suggesting a parameter called
returnValue
. - Fixes a crash when raising coco-tidy diagnostics on modules that have invalid names.
- If
Unreachable
is specified inlanguage.disabledWarnings
then this now correctly affects the verification. - Improves the behaviour of
popili
when executed on a Coco package that has no files. - Fixes a crash when exporting models that use state-machine inheritance via the EMF interface.
- Fixes a crash when creating encapsulating components that connect ports that do not have state machines.
- Fixes an issue that mean running code completion inside a monitor would not always respect any
setAllow
filters. - Fixes an issue that caused
@derive(Default)
on generic enums to require all of its generic parameters to be defaultable, even if only a subset of them were required in the first enum case. - Fixes an issue where ports that have
@unbounded
transitions that write to variables that are read by non-unbounded transitions would not be rejected. - Fixes a case where types declared inside monitors would cause code generation to crash.
- Fixes a crash when running code completion on types inside structs.
- Fixes a case where you could not pass an immutable reference to a struct field.
- Fixes a crash when running code completion on component constructors.
- Fixes a crash in the language server that could occur whilst editing Coco.toml files.
- Fixes a crash in the language server whilst typechecking invalid monitors that used arrays.
- Fixes a crash in the language server whilst running code completion on nested function calls.
- Fixes a crash when typechecking components that have incorrectly typed private variables.
- Fixes a case where the code completion documentation was incorrect for generic types.
- Fixes a case where code completion items involving
.
would be auto-selected in VScode, leading to confusing code completion behaviour. - Fixes an issue with running the language server on Windows where it would not reload files when they change on disk under some circumstances.
- Fixes several crashes with the language server whilst editing Coco.toml files.
- Fixes a case where diagnostics would not be updated inside the editor if a file was modified outside of the editor (e.g. via git).
- Fixes several issues that meant that working with Coco workspaces that contained invalid Coco packages would give misleading diagnostics.
- Fixes several issues creating support bundles, including incorrect Coco being printed, and also cases where the TOML files were not correctly synthesised making the resulting bundle malformed.
- Fixes an issue that prevented referring to trait instance functions without qualification even within the trait instance declaration.
- Fixes an issue that meant creating a support bundle in Eclipse would corrupt the names displayed in the assertions tree.
- Fixes an issue with
- Verification:
- Fixes a case where
purge
would not work correctly during verification if a part of a composite port was unsubscribed to on startup. - Fixes an issue that could cause the verification to fail with an internal error when using match statements with
a
variable pattern
and a customEq
instance. - Fixes several issues that could cause the junit output to be nondeterministic.
- Fixes a crash when displaying some complex
@eventually
counterexamples. - Fixes an internal error when verifying models that used function pointers stored in state parameters that included non-verified parameters.
- Fixes an issue with the simulator that meant it would not report errors raised during initialisation.
- Fixes a case where
- Log Replay:
- Fixes replaying logs from stdin against multiple monitors.
- Fixes a crash when displaying counterexamples for certain logs.
- Fixes a crash when displaying some counterexamples from specific monitors.
- Tooling
- Fixes a bug where the output of popili metadata would duplicate declarations.
- Fixes several issues in the values JSON schema relating to primitive values.
- Fixes the value of the
file
property of source locations when generating metadata usingmetadata --ast
; it is now relative to the Coco.toml file. - Fixes a crash when the Popili download website is unreachable.
- Fixes a rare crash when generating architecture diagrams.
- Fixes a case where
setAllow
did not generate a diagnostic when invoked on provided ports. - Fixes a crash when verifying models that contained trait instances that were infinitely recursive.
- Fixes the type of the timer id parameter in the generated C++ code to ensure it is consistently defined as
int32_t
rather than sometimes asint
. - Fixes a bug with formatting files that have CRLF line endings and have imports that need sorting.
- Fixes a bug extracting the proxy configuration on Windows that could cause the proxy to be ignored.
- Fixes renaming of static members.
- Fixes a crash when constructing invalid models that use the mixed runtime.
- Fixes a case where the format specifiers in format strings would be broken by the auto-formatter.
- VSCode:
- Fixes various issues that would result in diagrams opening over the top of editors.
- Fixes an issue that caused the architecture diagram to be blurry.
- Fixes an issue where panning one of the diagrams would also cause a click to be registered, leaving to editors opening unexpectedly.
- Code Generation:
- All:
- Fixes a bug that meant that
send_drain_queue
was generated multiple times in the generated code. - Fixes an issue with generating code for
await
that could lead to some unreachable code being generated. - Improves the handling of defaults on external types so that all generators are consistent with how they apply attributes related to initialisation.
- Fixes unused variables in the generated code for encapsulating components.
- Fixes a crash when generating code on models that use the
@implicitCast
attributes. - Fixes a crash when using
await
on components that have multiple required ports of the same type.
- Fixes a bug that meant that
- C++ Generator:
- Fixes an issue when generating mocks when function overloading is used.
- Fixes an issue that caused
valueOr
to not be compiled correctly in the generated C++ code when using C++11 or C++14. - Fixes a misleading error message when the
.clang-format
file contains an error. - Fixes a TODO that was incorrectly left in the C++ runtime header.
- Fixes an issue with the generated code when
generator.cpp.componentStyle
is set toHideImplementation
that would cause the code to not be compilable. - Fixes several bugs that could cause includes to be missing from the generated code. This would most commonly
affect uses of the
Log
trait. - Fixes several issues that caused the generated C++ code to contain unused variables under some configurations.
- C# Generator:
- Fixes a case where the
C#
profile was too strict and raised errors about name clashes that were not actually errors. - Fixes an issue where the C# profile would incorrectly report that an external type’s name clashed with its parent.
- Fixes an issued that prevented the generated code from compiling when multi-dimensional arrays of ports were used.
- Fixes an issue that would cause code generation to fail with filesystem errors.
- Fixes an issue where the generated code would contain errors relating to non-file-local types.
- Fixes a crash when generating code for Coco models that include an
unused()
handler with parameterised states. - Fixes an issue where the generated code incorrectly used
ref
in some cases. - Fixes a crash when generating code for Coco models that defaulted arrays of reference types.
- Fixes an issue that prevented the generated code from compiling when using multi-step port inheritance.
- Fixes an issue where
Result<T, E>
could not be defaulted whenT
is defaultable. - Fixes a crash when generating C# for Coco code where an external member function was mapped to a non-member function.
- Fixes a case where the generated C# would not compile because the auto-generated Timer enum would contain duplicated values.
- Fixes a case where the
- C Generator:
- Fixes several issues that could cause includes to be missing from the generated code. This would most commonly
affect uses of the
Log
trait.
- Fixes several issues that could cause includes to be missing from the generated code. This would most commonly
affect uses of the
- All:
The release notes for the test releases that led up to 1.5.0 can be found at 1.5 Pre-Releases. Relative to the final test release, this release contains the following changes:
New features:
- VSCode now includes support for the structure diagram from Eclipse, which summarises state machines and shows which events are permitted in which states. This is also integrated into the reachability counterexample viewer, so that reachability counterexamples can be viewed as an overlay on the structure diagram. Like other diagrams in VSCode, this diagram live updates as the code is updated.
Improvements:
- There is now a JSON schema available for the verification results output.
- The VSCode plugin will now work even when VSCode is opened on a workspace where the root does not contain a Coco.toml
file. If this is done, then as soon as
.coco
file orCoco.toml
file is opened, the VSCode plugin will process the corresponding Coco package. - In VSCode, the architecture and state diagrams now use the main VSCode UI font.
Bug fixes:
- Fixes several issues that would cause reachability to be incorrectly reported on state machines that use more than one step of state machine inheritance.
- Fixes a case where the simulator would fail to start in VSCode after fixing all counterexamples.
- Fixes a case where the generated C++ code would not compile if
headerOnlyRuntime = true
was specified.
1.4.7 (25/11/2024)¶
- Fixes an issue with the generated C and C++ code where the
generator.cpp.fileHeader
setting would not be respected for runtime files under some conditions.
1.4.6 (15/11/2024)¶
- Fixes an issue with the generated code that meant that characters would not be escaped correctly when logging strings. This affects all languages.
- Fixes an issue that would cause escaped null characters in string literals (i.e.