1.4 Pre-Releases¶

1.4.0-rc.1 (12/06/2024)¶

Breaking changes:

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

New features:

• 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’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 to language.standard 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).

• Coco now supports access control, which allows the accessibility 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.

  Coco supports the following access levels:

  • private: only usable in the containing context.
  • protected: only usable in the containing context, or in subtypes of it.
  • public(module): declaration is accessible within the current module only.
  • public(package): declaration is accessible within the current package only.
  • public: declaration is accessible to code in any package.

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

  [tool]
  selectedVersion = "1.3.11"
  

  then if Coco 1.4.0-rc.1 (or later) is invoked, it will automatically download 1.3.11 and execute the command using that version.

Several of the new features require the use of language.standard set to 1.2: 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.

Improvements:

• The structure viewer in Eclipse now takes setAllow and setAccess into account, making its summaries more accurate.
• The C# profile now has better support for rejecting trait instances that will result in uncompilable generated C# code, meaning that errors will be found earlier.
• VSCode caches architecture and state diagrams, meaning that re-renders should be faster if the diagram was recently drawn.
• The name of a component that appears in the logging will now contain the array index.

Bug fixes:

• Fixes a crash when mapToMember is misused with C#.
• Fixes a case where the generated code’s behaviour was incorrect when using a variable declaration pattern and also mutating the original value that was matched over after the match.
• Fixes a case where the typechecker would go into an infinite loop when typechecking some complex generic requirements.
• Fixes a crash when a generic trait instance contains unused type parameters.
• Fixes a case where the verification could crash when a counterexample was found.
• Fixes a crash when shutting down the language server.
• Fixes a case where the generated C++ code would not compile when generating code for certain trait instances.
• Fixes a bug that caused the typechecker to permit tagged enums to be converted to ints.
• Fixes a bug that meant that invariants inside states were not being typechecked.
• Fixes a crash when Eclipse or the VScode plugin were open for a long period of time.
• Fixes a crash when a malformed attribute is attached on an encapsualting component.

1.4.0-beta.10 (25/04/2024)¶

Bug fixes:

• Fixes an issue where the generated C# code would not compile if an equality comparison was performed on a simple enum in a generic context.

1.4.0-beta.9 (24/04/2024)¶

This is a re-release of 1.4.0-beta.8 to fix some packaging issues with the C# runtime. It otherwise includes no differences.

1.4.0-beta.8 (23/04/2024)¶

New features:

• C# generator:
  • The generated code now incorporates logging via a customisable Cocotec.Coco.ILoggable interface.
  • C# code is now correctly generated for Coco functions that use Coco’s Eq, Ord and Cast traits.
  • The runtime is now available as a Nuget package.
  • There is now a C# language profile that restricts Coco features that are not supported by the C# generator. This includes:
    • Detection of cases where the Coco code would copy values, but the generated C# code would not generate copies. For example, Array is a value type in Coco, but arrays are reference types in C# and therefore copies of arrays in Coco would only copy the reference in the generated C# code, leading to inconsistent behaviour.
    • Detection of cases where Coco’s generics are not compatible with C#’s generics.
• There is now a Vector2 module that aims to be more ergonomic than the Vector module. In particular, the Vector2 module only has one relevant size type, of type Bounded<0, maxSize, UInt>; in contrast, Vector uses that type and Bounded<0, maxSize-1, UInt>, leading to many casts.
• VScode plugin:
  • State diagrams are now viewable inside VScode via an inline Code Lens.
  • The overall Coco Platform status is now shown in the VScode status bar.

Improvements:

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

Bug fixes:

• Fixes an issue with the C# runtime code that would mean that timers could only be enabled once.
• Fixes an issue that caused the generated C# code to be uncompilable when a function returned Nil and the mixed runtime was being used.
• Fixes an issue that prevents the try operator being used in a compound expression (e.g. x?.y).
• Fixes an issue that would cause the language server to disagree with the editor about the canonical path to a file in the presence of symlinks, which could lead to various odd behaviours.
• Various fixes to improve the VScode plugin’s behaviour when the language server is restarted.
• Various fixes to the VScode architecture diagram viewer, particularly when a file is updated whilst the diagram is open.
• Fixes a case where editing the TOML file would cause Coco file editors to stop updating their diagnostics.
• Fixes an issue that prevented some elements of await transitions from being clickable in an editor.
• Fixes various crashes when viewing counterexamples in Eclipse on unusual errors.
• Fixes an incorrect diagnostic when an external implementation component is referenced are declared after their first use.
• Fixes a case where the 1.4 betas had inconsistent verification behaviour compared to the 1.3. This affected models where a nested state had several transitions with guards, but there was also a fallback transition in a higher state; in the 1.4 betas the transition would sometimes be reported as incorrectly illegal.
• Fixes an internal error when verifying traces with signals that contain data.
• Fixes an issue where the verification would crash if UInt was used as a parameter in a port.
• Fixes the use of mutable variables in simple awaits.
• Fixes various issues with using casts on types involving NonVerified, Slot and one of the Coco numeric types.

1.4.0-beta.7 (18/01/2024)¶

New features:

• VerifiedVector now implements the Iterable trait allowing vectors to be iterated over directly:

  var x : VerifiedVector<Bool, 2>;
  x.pushBack(true);
  for z in x {
    assert(z);
  }
  

• subscribe and unsubscribe can now be used inside monitors to dynamically determine which ports to receive events from.

Bug fixes:

• Remove some unused parameters from the C++ runtime header.
• Fixes an issue that could prevent the VScode plugin from obtaining a license.

1.4.0-beta.6 (10/01/2024)¶

New features:

• This includes an early preview release of a C# generator for Coco. This can be generated from the command-line by executing coco generate-csharp, or alternatively from the IDE by setting generator.defaultLanguage to "CSharp".

  Contact support@cocotec.io for further details if you are interested in trying the early releases of this feature.

• The VScode plugin supports showing architecture diagrams for encapsulating components. This is exposed via a Code Lens within VScode.

1.4.0-beta.5 (08/12/2023)¶

Improvements:

• If an event is always illegal, then the generated C or C++ code will no longer contain unreachable lines of code after the abort.
• In the generated C++ code, components will now contain explicit destructors.
• The C++ runtime header now always explicitly initialises variables to avoid false positives from static analysis tools.
• The generated code will favour using constants over mutable variables for intermediate values.
• Bounded support has been improved to ensure that complex calculations involving bounded are only bounds checked when the resulting store happens.

Bug fixes:

• Fixes a crash when verifying state machines that include an offer with only an otherwise clause.
• Fixes several cases where the generated code for await would contain variables that were not used, leading to compiler warnings.
• Fixes several issues that would result in Eclipse appearing to hang when running code completion or format-on-save on large files.
• Fixes a case where an internal error would be raised when verifying models containing immutable references.

This version also incorporates the bug fixes relased as part of 1.3.12.

1.4.0-beta.4 (08/11/2023)¶

Improvements:

• Added an option to explicitly set a proxy server, instead of using autodetection.

Bug fixes:

• Fixes various issues with the licensing system that could cause Eclipse to become unresponsive.
• Fixes a crash when declaring a variable of function reference type that has no default value.

1.4.0-beta.3 (03/11/2023)¶

Improvements:

• Improves the licensing system so that more information is provided inside Eclipse, and also more actions are automated in the background.

1.4.0-beta.2 (18/10/2023)¶

Improvements:

• Log files can use struct-like syntax to specify arguments by name for function calls, signals, and enums. Further, non-verified values can be omitted entirely using this syntax.

Bug fixes:

• Fixes an issue that would cause diagnostics that were emitted during verification to be suppressed.
• Fixes a crash when typechecking complex generic signatures.
• Fixes a crash when performing code completion on setAllow in monitors.
• Fixes an incorrect code completion when performing code completion on setAllow in monitors.
• Fixes an internal error when replaying logs on monitors that monitor ports that include &out parameters and return values.
• Fixes an issue in the generated code that would result in log entries not including . in the names of nested ports.

1.4.0-beta.1 (26/09/2023)¶

New features:

• This version contains a early preview release of new functionality that allows the Coco Platform to analyse log files using monitors. A monitor is a new declaration within Coco 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 defined 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.

  Contact support@cocotec.io for further details if you are interested in trying the early releases of this feature.

Improvements:

• 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.
• The semantic highlighting has now been improved, particularly for complex patterns.
• Ord can now be defined on non-verified external types.

Bug fixes:

• Fixes a case where errors regarding port inheritance would be located in incorrect places.