Release Notes¶

1.4.2 (23/08/2024)¶

Improvements:

• The parser now emits better diagnostics when using language standard 1.2 and the name of a function in a port clashes with one of the new reserved names.
• The parser now generates clearer diagnostics if attributes are specified after a transition name.
• The bundled Coco examples are now compatible with language standard 1.2.
• New projects created in Eclipse are now created with language standard 1.2.
• The log replay code now supports explicitly writing nil when a parameter of type Nil is expected.
• Improved the truncation of labels in the architecture diagram to make it clearer which options are applied.

Bug fixes:

• Fixes an issue that caused rename to not rename fields inside struct literals.
• Fixes a case where the typechecker would not automatically derive an instance of Eq for structs.
• Fixes a crash when using @derive(NonVerifiedOrd).
• Fixes a case where the language server would not report diagnostics on Coco.toml files.
• Fixes a crash when verifying models where generic value parameters are used as expressions.
• Fixes a crash when verifying some models that used transition labels on spontaneous transitions.
• Fixes the behaviour of the comparison operators on UInt on comparisons with numbers outside the range of Int.
• Fixes a case where the verification would fail with an internal error if trait instances were only required in type contexts.
• Fixes a crash when running the simulator on some complex Coco code.
• Fixes a case where the formatter would insert extra spaces around [ inside array literals.
• Fixes a case where the formatter would not insert newlines if a state variable did not have an initialiser.
• Fixes an issue with the formatter that would cause it to incorrectly format code around state invariants.
• Fixes the behaviour of undo in Eclipse.
• Fixes an issue that caused the line numbers displayed in Eclipse after clicking on code lenses to be off by 1.
• Fixes the behaviour of the + and - buttons did not work in Eclipse on workspace projects.
• Fixes an issue where the generated C code would have different behaviour to the Coco code when for loops were used where the for loop’s body also modified the contents of the array being iterated over.
• Fixes an issue that caused the generated C++ and C# to be uncompilable if signals were overloaded in Coco.
• Fixes an issue that caused unused coco_drain_queue() functions to be generated in the object-orientated C code, leading to C compiler warnings.
• Fixes a case where the generated C# code would not compile if @derive was used on structs with generic value parameters.
• Fixes a case where the generated C# code would not compile if Coco Vectors were compared for equality.
• Fixes a case where the generated C# would not compile due to ref being incorrectly added on types marked with @CSharp.referenceType.
• Fixes a case where the C# profile was too permissive and did not catch Coco code that would different semantics than the generated C# code.
• Fixes a case where the generated C# code would not compile when generic ranges were used (e.g. Range<T>).
• Fixes an issue with the C generator that would cause it incorrectly use . instead of -> when invoking methods on arrays.
• Fixes the behaviour of the generated C++ code on ranges where the upper bound is greater than the lower bound (e.g. range(4, 2)).
• Fixes a rare crash that could occur at any point.

1.4.1 (06/07/2024)¶

Improvements:

• Older Coco Platform plugins for Eclipse can now be easily installed using the normal Eclipse plugin installation.
• Documentation is now available for the Log trait, format strings and the log format.

Bug fixes:

• Fixes several issues with the generated C++ code that would cause the generated code to be not compilable when the Coco standard is set to 1 or 1.1.
• Fixes an issue with the generated C++ code that could lead to errors about ambiguous operator== overloads.
• Fixes an issue with the generated GMocks that caused them to be uncompilable under certain conditions.
• Fixes several warnings that MSVC would report in the C and C++ runtime headers.
• Fixes an issue that led to transition labels being rejected on nondet clauses outside of state machines.
• Fixes an issue that caused access specifiers to be incorrectly accepted on import declarations.
• Fixes an issue with the language server that could cause errors or warnings to remain in the editor after they have been fixed.
• Fixes an issue with the language server that could cause warnings in Coco.toml files to not appear after a modification to them is made.
• Fixes an issue with the language server that could cause warnings and errors to not appear when a project is reopened in Eclipse.
• Fixes an issue that causes the log replay to not work correctly on parameters of type Nil.
• Fixes a crash when handling malformed ports or components that incorrectly inherit from themselves.
• Fixes an internal error when verifying models that use string literals as module-level constants.
• Fixes an issue with validating access specifiers inside ports which could lead to correct code being rejected.
• Fixes an issue with the Coco Platform Eclipse plugin packaging that would allow the UI feature to be installed without the API feature.

1.4.0 (28/06/2024)¶

Breaking changes:

• The Eclipse plugin now requires at least Eclipse 2023-09.

New features:

• Language:

  • This version introduces a new language standard, Coco 1.2. This standard reserves some additional keywords and also includes some minor changes to the generated code to facilitate new features. See Migrating to Coco Standard 1.2 for advice on how to migrate to the newer language standard. Note that the Coco Platform 1.4 is fully compatible with the Coco Platform 1.3 if language.standard is not modified; the upgrade steps only apply when you want to change the language standard to 1.2.

  • Coco now includes format strings which allow strings to be constructed at runtime that include pretty-printed values. For example:

    function sayHello(name : String) : String = $"Hello {name}"
    

    If sayHello("Tom") is invoked, the string "Hello Tom" will be returned. This uses a new Log trait to pretty-print each value in both a machine and human readable format. This is supported only with language.standard set to 1.2.

  • Coco now supports access control, which allows the visibility of declarations to be controlled. For example, this can be used to make private utility functions that are not exported from modules:

    private function myUtility() : Nil = …
    

    It can also be used to mark entire modules as private (by using private module) so that the module is not accessible from outside of that package. Visibility specifiers are also checked for consistency meaning, for example, that public functions cannot expose private types.

    See Visibility for further details.

  • Coco now allows requirements over events to be formalised via monitors. A monitor is a new declaration that is able to monitor events over ports. For example, the following Coco defines a monitor that insists that a call to emergencyHalt over one port will result in a call being made on another port too:

    @runtime(.MultiThreaded)
    monitor Propagates {
      val top : Provided<P>
      val bottom : Required<P>
      machine {
        // Ignore the end of the function calls
        end(bottom.emergencyHalt(), _) = {}
        end(top.emergencyHalt(), _) = {}
    
        state WaitForTop {
          // Wait for the top
          start(top.emergencyHalt()) = setNextState(WaitForBottom)
        }
        state WaitForBottom {
          start(bottom.emergencyHalt()) = setNextState(WaitForTop)
        }
      }
    }
    

    Such monitors can be used to analyse log files that are in a standard Coco format, and the tool will show an error whenever the log file contains an event that is deemed to be illegal by the monitor.

• Generated Code:

  • Coco’s auto-generated logging is now able to log the values of parameters, return types, and state parameters. For example:

    > system.halLight[0]: client.onOff{isOn=true}
    

    Note the array indexes are now included, and parameters are also logged.

    To use this, switch language.standard to 1.2 and set generator.cpp.logValues to either “Always” (meaning that an instance of Log is required for all parameters and return values, or an error will be raised) or “WhenAvailable” (meaning that parameters or return values that have a Log instance will be logged).

    This logging format is natively supported by the log analysis tool used for monitors. The original log format is still used when generator.cpp.logValues is set to “Never”. This format can be useful in situations where the overhead of logging values would be too great.

  • The Coco Platform now includes a C# generator that generates standards-compliant C# 12 compatible code. This supports all features of Coco, including the new format strings and value-based logging.

• Tooling:

  • The coco command-line tool and the VScode plugin now incorporate an automatic downloader that will download the correct version of the Coco Platform based on the tool.selectedVersion setting. For example, if the Coco.toml file contains:

    [tool]
    selectedVersion = "1.3.11"
    

    then if the Coco Platform 1.4.0 (or later) is invoked or used in VScode, it will automatically download 1.3.11 and use that version instead.

Improvements:

• Language:
  • There is now a Vector2 module that aims to be more ergonomic than the Vector module. See Vector2 for further details.
  • VerifiedVector now implements the Iterable trait allowing vectors to be iterated over directly.
  • Integers are more ergonomic, as it is now possible to cast directly between a Bounded and any other integer type, rather than having to use two separate casts like before.
  • await is now allowed to be used inside signal handlers, providing they don’t use inherit.
  • Warnings are now generated for unused private variables and constructor parameters.
  • The time construction functions (e.g. seconds) now accept either UInt or Int.
  • Ord can now be defined on non-verified external types.
  • Bounded support has been improved to ensure that complex calculations involving bounded are only bounds checked when the resulting store happens.
• Generated Code:
  • If an event is always illegal, then the generated C or C++ code will no longer contain unreachable lines of code after the abort.
  • The pre-built loggers provided alongside the runtime libraries can be configured to also log timestamps with each message.
• Tooling:
  • General:
    • Workspaces can now be nested; i.e. a workspace can contain other workspaces.
    • A warning is now raised when a newer language.standard is available.
    • A warning is now raised when language.profiles is inconsistent with generator.defaultLanguage.
    • Added an option to explicitly set a proxy server, instead of using autodetection.
    • A warning is now raised when a newer language.standard is available.
    • A warning is now raised when language.profiles is inconsistent with generator.defaultLanguage.
  • Eclipse:
    • The structure viewer in Eclipse now takes setAllow and setAccess into account, making its summaries more accurate.
  • VScode:
    • State diagrams are now viewable inside VScode via an inline Code Lens.
    • The VScode plugin supports showing architecture diagrams for encapsulating components. This is exposed via a Code Lens within VScode.
    • The overall Coco Platform status is now shown in the VScode status bar.
    • The semantic highlighting has now been improved, particularly for complex patterns.

Bug fixes:

The release notes for the test releases that led up to 1.4.0 can be found at 1.4 Pre-Releases. Relative to the final test release, this release contains the following changes:

Improvements:

• VScode will now automatically download whatever version of the language server is set by the tool.selectedVersion setting.
• Workspaces can now be nested; i.e. a workspace can contain other workspaces.
• The consistency of access specifiers in Coco is now checked. For example, this means that a function on a port cannot return a private type declared in the port.
• The builtin loggers for C, C++ and C# can now be configured to log timestamps with each message.
• The builtin loggers for C, C++ and C# have been improved to allow parts of them to be reused in custom logger implementations.
• The C# profile has been improved to allow some local variables of reference type to be returned in cases where previously, they were not.
• It is now possible to customise the top-most access specifier used by Coco in the generated C# code. If generator.csharp.publicAccessSpecifier is set to "Internal", then the generated code will use the internal access specifier in C# wherever possible.

Bug fixes:

• Fixes several issues with the formatter that would cause it to misformat code.
• Fixes an issue that would cause the range expression of for loops that contain communication to be evaluated multiple times.
• Fixes an issue that would cause the range expression of for loops to never be evaluated if the array is empty.
• Fixes several issues that would cause internal errors when verifying models that use non-verified data in certain ways.
• Fixes an issue that meant that attributes on transitions were not clickable inside VScode or Eclipse.
• Fixes several focus-related issues with the state and architecture diagram in VScode.
• Fixes a crash when using function pointers to trait instance methods.
• Fixes an issue where traits could be used as types in various places they should not have been.
• Fixes an issue where specialisation arguments were ignored during typechecking.
• Fixes several crashes on code completion.
• Fixes an issue where if @derive(NonVerifiedEq) was used, the resulting trait instance was not available.
• Fixes a crash when rendering state diagrams of state machines that combine inheritance with entry actions.
• Fixes a case where the generated code contained unused variables.
• Fixes an issue in the generated C++ code that would cause the generated mocks to be uncompilable when the parameter or return types contained commas.
• Fixes an issue that would cause the generated C++ code to multiply evaluate the range expression of a for loop when g++ 4.4 compatibility is enabled.
• Fixes a crash when viewing certain counterexmaples.
• Fixes an issue that would incorrectly allow NonVerifiedEq to be used as part of a variable pattern.
• Fixes a crash when opening a file that has an invalid name in either Eclipse or VScode.

1.3.13 (23/03/2024)¶

Bug fixes:

• Reduces the amount of memory used after verification of large projects has completed.
• Fixes an issue where isValid or isInvalid could be used in a component outside of an assertion, which could result in different behaviour at runtime to the verified behaviour.
• Fixes an internal error when verifying models that include structs with no verified fields.
• Fixes a crash when generating code where break was used in conjunction with match.
• Fixes some mismatches between the Coco vector types, and their corresponding methods in the Coco C++ runtime.
• Fixes a case where the verification could fail with a user error, but no diagnostic was generated.
• Fixes an issue that meant that external implementation components inside nested encapsulating components could not be accessed in the generated code.
• Fixes an issue that would mean that @ignore would not work on nested functions in structs, enums, or external types.
• Fixes a case where invalid encapsulating components would be accepted. Specifically this affects encapsulating components that use the single-threaded runtime, have a port that is shared, and where some sharing of implementations occurs across the boundary of nested encapsulating components. In such cases, the validation was inconsistent: if the nested encapsulating component boundary was removed, the component would be rejected, but it was incorrectly accepted with the nested encapsulating component boundary in-place.

1.3.12 (08/12/2023)¶

Bug fixes:

• Fixes an issue that would prevent the state machine diagram from being displayed. This would mostly have affected complex state machine diagrams with many nested states.
• Fixes a case where the generated C or C++ code would not correctly match the Coco code. Specifically, the generated code could omit a required break statement inside a switch meaning that the generated code would incorrectly fall through to the next switch case.
• Fixes several related issues that could cause the verification to ignore runtime errors (e.g. no matching clause of a match expression, or divide by zero, etc) in arguments of the log function or in non-verified fields of structs.
• Fixes the generated code being uncompilable when UInt is explicitly defaulted. Note that this fix will result in UInt being mapped to unsigned`in C++, rather than :cpp:`unsigned int. This has no impact on the semantics, but will result in a diff in the generated code wherever UInt is used.
• Fixes poor quality code completion suggestions for sending signals in ports.
• Fixes the typechecker silently failing when an implicit member expression is passed to a &mut or &out parameter.
• Fixes a crash when parsing state machines that use some of the new Coco 1.1 keywords as the names of functions in ports. This version also improves the diagnostics that are generated when this happens.
• Fixes an issue that would mean that an error could be reported about @derive(Default) being impossible, but typechecking would still be considered as succeeding.

1.3.11 (26/09/2023)¶

Bug fixes:

• Fixes a crash when using static functions via generic type aliases.
• Fixes a crash when using package.workspace with certain directory structures.
• Fixes a case where using break inside await would result in the generated C++ code not compiling.
• Fixes a crash when loading Coco packages that include .coco files with multiple invalid file components.
• Fixes a crash when viewing counterexamples that use &mut parameters inside a while loop.
• Fixes a case where diagnostics would not be raised when an import was not found but language.packageScopedImports was set.

1.3.10 (08/08/2023)¶

Bug fixes:

• Fixes a case where verification of expressions such as e.fn() where fn is a member function on a non-verified type, and e has a verification side effect, would incorrectly pass.
• Fixes a crash when parsing patterns that contain a minus followed by a non-integer literal.
• Fixes a crash when generating code via the API.
• Fixes a case where the generated C++ code would not compile when using a type alias for a Bounded that has a non-zero lower bound.
• Fixes a case where the generated C++ code would not compile due to the generated enum sentinel function.

1.3.9 (19/07/2023)¶

Bug fixes:

• Fixes an issue that could cause single-threaded components that have arrays of provided ports to incorrectly pass the verification, even if a single transition sends a signal to two different elements of the array.
• Fixes an issue that could cause the C and C++ generators to be nondeterministic and reorder declarations in different invocations.
• Fixes a crash when running verification using the API.
• Fixes an exception in Eclipse when viewing certain multi-client counterexamples.
• Fixes a case where the cloud verification icon in Eclipse would appear as connected despite there being an error.
• Fixes a crash when generating metadata on Coco files that contain anonymous state machines.
• Fixes a crash when typechecking malformed encapsulating components.

Improvements:

• Added coco --output-unchanged-files to improve compatibility between Coco’s code generation and timestamp-based build systems, such as make.

1.3.8 (28/06/2023)¶

Bug fixes:

• Fixes an issue introduced in 1.3.7 that would prevent code from being generated if multiple .coco files produce empty generated C or C++ files.
• Fixes an issue where the generated C or C++ code for an encapsulating component would require an Arguments struct even though all external components were given concrete external implementation components inside the encapsulating component.
• Fixes a crash in the language server when viewing certain malformed files.

Improvements:

• Improves error reporting when the verification server is unreachable due to issues authenticating to proxy servers.

1.3.7 (23/06/2023)¶

Bug fixes:

• Fixes an issue that would cause the Coco Platform to crash whilst rendering architecture diagrams of encapsulating components that instantiated other encapsulating components and then specified external implementation components for external components.
• Fixes an internal error that could occur whilst verifying Coco files that a generic struct that itself contained a field that used a generic value parameter, and where the struct derived the Eq trait.
• Fixes an issue that would cause Coco to generate effectively empty header or implementation files even when generator.cpp.outputEmptyFiles was false.
• Fixes an issue that would prevent patterns being passed that contained negative numbers.
• Fixes several minor issues in the Coco tutorial and improves the clarity of some of the examples.

1.3.6 (06/06/2023)¶

Bug fixes:

• Fixes an issue that could cause Coco to crash when connecting via authenticated proxies.

1.3.5 (05/06/2023)¶

Bug fixes:

• Fixes an issue that would mean that break clauses would sometimes be missing in switch clauses in the generated code. This could have occurred when a match clause was used as the value of a function, there were precisely two clauses in the match, and the value of the match clause contained an if and an else-if.
• Fixes an issue that would mean that a C++ implementation file would still be generated when generator.cpp.headerOnlyPorts was set and generator.cpp.componentStyle was set to HideImplementation.
• Fixes an issue that would mean that the typechecker would incorrectly give errors about unconnected ports on unconnected fields of mocked external components.
• Fixes a case where Coco’s typechecker would sometimes fail without raising any diagnostics when a constant was used as a type parameter, but the constant’s value was not computable at compile time.
• Fixes a case where Coco’s typechecker would incorrectly not give a diagnostic when an encapsulating component has a constructor, but the constructor is not used when instantiating the encapsulating component in another encapsulating component.
• Fixes an issue that would cause Eclipse to offer to upgrade Coco 1.1 compatible projects to Coco 1.0.

1.3.4 (24/05/2023)¶

Bug fixes:

• Fixes an issue where the C++ generator would crash when generating trait instances that contained external functions that were mapped using @CPP.mapToValue.

• Fixes an issue where the generated code would be incorrect in the case that an enum is being matched over, and the value that is being matched over is mutated before one of the matched fields is extracted. For example, consider:

  match (v) {
    .A(x) => {
      v = .B;
      assert(x == 2);
    }
  }
  

  In the above, the assertion would incorrectly fail because reading x would read the value currently stored in v, instead of the value stored in v at the time the match was evaluated.

1.3.3 (23/05/2023)¶

Bug fixes:

• This revises a fix made in 1.3.2 to address an issue with the order in which function arguments are evaluated in the generated C++ code. Specifically, this change restores the behaviour of 1.3.0 so that external functions are not considered to have any side effects beyond those that are explicitly modelled in Coco. This version also introduces a new attribute called @globalSideEffects which can be applied to external functions to indicate that the external function has side effects beyond those that are modelled in Coco. For example, given f(g(), h()), if g and h are declared as:

  @globalSideEffects
  external function g() : Nil = {}
  @globalSideEffects
  external function h() : Nil = {}
  

  then Coco will ensure that g() is always evaluated before h() in f(g(), h()), even though the C++ semantics does not guarantee this.

1.3.2 (22/05/2023)¶

Bug fixes:

• Fixes a case where the generated C++ code would evaluate the arguments of a function call in a different order than as specified by the Coco semantics. This would have affected a function call of the form f(g(), h()) where both g() and h() were calls to external functions that had invisible side-effects (from Coco’s perspective).
• Added a workaround for users who are affected by the increased checks made on single-threaded multi-client encapsulating components. Contact support@cocotec.io for further details if you are struggling with errors of the form: multi-client single-threaded components cannot share components.

1.3.1 (15/05/2023)¶

Bug fixes:

• Fixes an issue that could cause the output of the code generator to differ when code was generated on different machines.
• Fixes a crash when verifying state machines that included a direct return as a transition, and where the direct return directly involved communication (e.g. p.fn() = r.fn()).
• Fixes a crash when verifying models that passed a slot as an &out or &mut parameter before another argument that directly involved communication (e.g. r.fn(&slot, r2.fn())).
• Fixes an issue that caused coco format --verify to output misleading diffs in case the only change was the addition of a trailing newline.
• Fixes an issue that would cause Trace to be a reserved name even when using std == "1".
• Fixes an issue that would cause coco to write to files inside the user’s home folder even when instructed not to.
• Fixes an issue that would prevent some continue blocks from having the correct behaviour during verification.

1.3.0 (05/05/2023)¶

Breaking changes:

• A bug has been fixed that would mean that parameters whose type is marked with @mustUse, such as Result<T, E>, could be ignored by the function that uses them without generating an error, as originally intended. For example, the following code would not generate any errors:

  state S {
    rServer.fnCallback(res : Result<T, E>) = {}
  }
  

  This code will now result in an error under Coco 1.3. To fix this, either use res in some way, or if the error is not relevant, then the error should be discarded using discard(). For example:

  state S {
    rServer.fnCallback(res : Result<T, E>) = res.discard()
  }
  

• 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, or to introduce a proxy component between the port p and r in the above example.

New features:

• Language:

  • This version introduces a new language standard, Coco 1.1. This is a minor change versus 1.0 and just reserves additional keywords to allow for future enhancements. The new keywords are abstract, await, inherit, monitor, trace and verify; if your code uses any of these as the names of any construct then you will need to rename them when upgrading to Coco 1.1. We encourage all users to switch to Coco 1.1 as soon as possible to ensure their code will be compatible with future enhancements. To do so, modify standard = "1" in the Coco.toml file to standard = "1.1".

  • 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 compound 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 the use of the Coco 1.1 language standard.

  • 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.

  • 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.

  • Coco now supports unsigned integers via the UInt type.

  • 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 unknown 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.

  • Transitions, nondet clauses, await clauses and offer clauses can now be given names:

    StableFnCall: p.fn() = nondet {
      StableFnCallOk: true,
      StableFnCallFailure: false,
    }
    

    These names will be used by Coco in counterexamples.

• Tooling:

  • 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.

    This is particularly useful for projects that consist of a large number of Coco packages.

  • Apple Silicon is now a fully supported platform, including inside Eclipse, the CLI tooling, and VScode.

  • Code completion now works inside Coco.toml files and suggests additional settings, and values of enums where appropriate.

  • 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 equivalent 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.

    • ReadabilityOfferIf: when an offer is used where a if-then-else is equivalent, the tool suggests using if in order to improve readability.

    • 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.

  • 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.

Improvements:

• Code Generators:

  • @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 or C++ macro that results in a statement, rather than an expression.

  • @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.

  • 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.

  • Improved the error messages when generating code that refers to static vals that do not have a mapToValue annotation.

• C Generator:

  • The generated C code will now comply with -Wstrict-prototypes.
  • Added a compile-time version check for the C runtime.

• C++ Generator:

  • 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().
  • 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.
  • 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.

• Eclipse:

  • 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.

• Language:

  • @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.
  • 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.
  • Add a warning if a variable is referenced but its value is not used.
  • 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>.
  • Attributes can now be applied to an entire module, rather than just one declaration.
  • 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>.
  • 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 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 typechecker’s handling of break and continue inside blocks to provide better error messages in case of malformed Coco programs.
  • External types can now have member functions without having data members.

• Tooling:

  • 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 a setting package.generateCode that can be used to prevent code begin generated from a package. This can be used for utility packages that should never have their code directly generated.

  • --stats-json can be used to output simple statistics about the resources an execution of the command-line tool took.

  • 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.

  • Coco’s language server now supports workspace-wide symbols searches in both VScode and Eclipse.

  • Improved compatibility with new Eclipse versions which was causing Eclipse to generate a warning about the encoding not being specified.

  • 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
    

  • 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 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).

  • Improved the formatter to improve handling of long nondet expressions where the trailing comma has not been specified.

  • 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).

  • 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.

  • The command-line tool now only draws encapsulating components, rather than all components.

  • The support-bundle command now compresses its output.

  • Coco now loads TLS certificates from the system certificate store on Windows.

• Verification:

  • Coco’s remote verification is now enabled by default.
  • 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.
  • The command-line verification can now output json results and junit results in parallel to specified files.
  • The verification cache now ignores irrelevant settings from the Coco.toml file, meaning that results should more often be cached.
  • The remote verification backend now distuinguishes between out-of-memory and timeout errors.

Bug fixes:

• C++ Generator:
  • Fixes some missing const annotations in the C++ runtime header.
  • Fixes a case where the generated code would not compile when using arrays of external implementation components.
  • Fixes several crashes when generating code fails due to a filesystem error.
  • Fixes an issue that would prevent the generated C++ code from being compiled when using clang with older versions of libstdc++.
  • Fixes a case where inlay hints could be doubled if an implicit cast was used.
  • Fixes a crash when generating code using await on components that contained arrays of ports.
• Language:
  • Fixes an issue that meant that @ignoreWarning(.DeadState) had no effect when applied to a state machine.
  • Fixes an issue that could cause user-defined attributes to be dropped on optional nodes.
  • 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 case where Coco would incorrectly allow the same module to be imported multiple times.
  • Fixes a case where the parser would not parse calls on struct literals (e.g. S{x = 2}.f()).
• Tooling:
  • Fixes a crash when opening EMF-produced ASTs where an attribute has the wrong number of arguments.
  • Fixes a crash when performing renames.
  • Fixes a crash when performing code completion on struct literals.
  • Fixes a crash when performing code completion on arrays of ports.
  • Fixes a crash when performing code completion on generic types that include incorrect literal types.
  • Fixes an issue that would cause the inlay hints to flick on and off in VScode.
  • 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 a crash when loading certain malformed files in the language server.
  • Fixes the semantically-aware rename calculation when renaming module-level variables.
  • Fixes a case where subprocesses spawned by coco outlive coco itself.
  • 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 a case where Eclipse fails to show the code lenses for a port or component.
  • Fixes a crash when running semantic highlighting on complex generics.
  • Fixes a crash when loading a workspace that contains a package with no files.
  • Fixes a crash when loading a package that is in a workspace that is invalid.
  • Fixes an issue where the generated include files would be incorrect for the generated gMocks.
• Verification:
  • Fixes a case where purge() would not work correctly during verification when combined with port inheritance.
  • Fixes a crash when verifying state machines that consume too much data. A clean readable error is now reported.
  • Fixes an internal error when verifying models that use Slot<T> with a T that contains member functions but no fields.
  • Fixes an issue that would prevent non-verified types with @mustUse from being used as arguments to functions or signals in a port.
  • Fixes a crash when verifying models that convert NonVerified<Int> to Duration.
  • Fixes improves the behaviour of the tool when the verification cache is unresponsive.
  • 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.

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

• Stateless ports are no longer required to not be used in a shared way when using single-threaded multi-client.
• Improves the behaviour of the parser when a feature is used from a newer language standard without modifying the TOML file.
• Vector has been moved to 1.1, meaning that user-defined modules called Vector will not clash with the new builtin standard.
• Improves the behaviour of package.preventCodeGeneration and renames it to package.generateCode.
• Improves error messages when usage of await is prohibited.
• Added an option to ReadabilityOfferIf to force the rewritten code to use a block.
• Fixes several errors with the verification of await that could cause crashes or incorrect counterexamples, particularly when involving execution states, @slow or @unbounded.
• Fixes several crashes when writing complex functional-like code where inner arguments used nondeterminism.
• Fixes a case where a counterexample could not be displayed.
• Fixes a case where the variable highlighter would not highlight variables consistently.
• Fixes a crash when Coco detects a cycle within the encapsulating component.
• Fixes an issue that would cause the list of modules inside Eclipse to not be sorted sometimes.
• Fixes a crash when an await is malformed.
• Fixes the warning raised when a port is unconnected to correctly refer to the unconnected ports when part of an array is unconnected.
• Further improves compatibility of the generated C++ code with pre-C++11 compielrs.

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 transforms 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.