1.2 Pre-Releases

1.2.0-beta.16 (18/05/2022)

Breaking changes:

  • The object-orientated C generator now takes the Arguments struct by pointer, rather than by value. To upgrade, use &arguments rather than arguments when calling the _create function.

New features:

  • 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, and that very large verification jobs (e.g. those with several hundred 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.
  • 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.

Improvements:

  • Documentation has been added for:
  • Diagnostics have been improved when using multiple port inheritance wihere the same declaration is defined in more than one base port.
  • The command-line verification tool now provides better output if there is a connection error when running verification remotely.
  • The code completion snippets produced by the language server have been improved to remove the types, making them easier to work with.

Bug fixes:

  • 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 an issue that would cause the generated C++ code to be incompilable with g++4.4 when using multiple inheritance. This release also adds a profile, C++MSVC that can be used to prohibit Coco constructs that cannot be compiled when using MSVC, such as diamond inheritance.
  • 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.
  • Fixes a crash when using the language server on malformed files that included references to member functions without calling them.

1.2.0-beta.15 (21/04/2022)

Improvements:

  • Code completion on state machines now takes into account setAccess and setAllow calls.
  • Cast is now fully supported when generating C++, and will correctly generate C++ code corresponding to user-defined cast instances.

Bug fixes:

  • Fixes a crash when generating code containing external implementation components.
  • Fixes a bug that would cause code completion for arrays of provided or required ports to suggest invalid Coco code.
  • Fixes a case where the verification would report an internal error with @satisfiesEventually when two ports contained EventuallyAssumption s with the same name.
  • 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 an issue with proxy detection on RHEL6.
  • 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.

1.2.0-beta.14 (14/04/2022)

New features:

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

Improvements:

  • Coco’s generated mocks now include send_ helper functions to easily send signals, including via the GMock Invoke action.

Bug fixes:

  • Fixes a crash that occurred when trying to render the architecture diagram for very large encapsulating components.
  • Fixes an issue that would cause become to be incorrectly rejected when used with single-case enums.
  • Fixes an issue with the Eclipse syntax highlighting that would cause identifiers that contained a Coco keyword (e.g. port_var) to have incorrect highlighting.
  • Fixes several issues with the pretty-printer that would cause the support-bundle command to generate incorrect Coco files.

1.2.0-beta.13 (13/04/2022)

New features:

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

Improvements:

  • Code completion now works for fields within external implementation components.
  • The rules on where become is allowed have been slightly relaxed to permit arguments types to differ regarding simple enums, providing the enums take up the same amount of space.

1.2.0-beta.12 (12/04/2022)

Improvements:

  • Component constructors can now be initialised inline via e.g. val c : Comp = Comp(2).
  • 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.useHierarchialNames has been added that allows users to choose 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.

1.2.0-beta.11 (06/04/2022)

Improvements:

Bug fixes:

  • 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 case where unscoped enums using @CPP.mapToEnum would be incorrectly qualified.

1.2.0-beta.10 (02/04/2022)

Improvements:

  • Coco now supports the GNU89 standard for generated C code, which can be specified via standard = "GNU89" in the Coco.toml file.

Bug fixes:

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

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

1.2.0-beta.9 (01/04/2022)

New features:

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

Improvements:

  • The object-orientated C generator now supports timers.
  • 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.
  • Coco’s C runtime header is now more compatible with C89 compilers.

1.2.0-beta.8 (29/03/2022)

Improvements:

  • Diagnostics when component constructors have not been specified are now clearer and mention which component was missing a constructor call.
  • C.mapToEnum now has an additional option to specify whether the enum is typedef’d or not in C.
  • The generated object-orientated C code can have component observers attached to allow key lifecycle events to be observed.

Bug fixes:

  • Fixes a bug that caused incorrect code to be generated for implmeentations of != when using notEquals via a function pointer.
  • Fixes an issue that would have caused verification to emit user errors when verifying components using component constructors.
  • Fixes an issue that caused -e to be parsed incorrectly when there was no space between - and e.

1.2.0-beta.7 (23/03/2022)

Improvements:

  • Coco will not format files that include source control conflict markers, making it easier to merge Coco files inside VScode and other editors.
  • The C profile now bans the use of function overloading and empty structs.

Bug fixes:

  • Fixes loading several projects into the same Coco workspace inside the language server where the projects all contain files with the same name.
  • Fixes a crash when using SymmetricArray with large cardinalities.
  • Fixes a case where the generated C++ code would not compile when using multiple inheritance.
  • Fixes a case where the generated C could would not compile when using inheritance.
  • Fixes several rare crashes with the language server.

1.2.0-beta.6 (21/03/2022)

New features:

  • 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. For example:

    component Shared {
  val clients : SymmetricArray<Provided<P>, 200>
  machine {
    state Idle {
      p[val i].fn() = { setNextState(Running(i)); return true; }
    }
    state Running(i : SymmetricArrayIndex) {
      after(seconds(1)) = {
        p[i].sig();
        setNextState(Idle);
      }
    }
  }
}

    The use of SymmetricArray will enable Coco to improve the performance of the verification. To ensure that this is sound, Coco will automatically check that the component satisfies several conditions before running the verification.

  • Component constructors can now 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.

Improvements:

  • 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 internal error that was raised when using port inheritance on ports that include only functions.
  • Fixes an issue that would cause code completion results to be filtered too heavily.
  • Fixes a crash when parsing files that accidentally declare provided or required ports inside state machines.
  • Fixes a crash when typechecking files that contained encapsualting components that connected composite ports using port inheritance, where one side of the connection was of a base type and the other side was of a derived type.
  • Fixes an issue that caused code lenses to flicker on-and-off in Eclipse and VScode, or to be placed on incorrect lines.
  • Fixes several crashes in the language server:
    • When parsing files that included array transitions with invalid syntax.
    • When parsing files that included uninstantiated generics.
    • When executing actions that require project-wide information (e.g. code lenses or rename).
    • When parsing files that were deleted in parallel to the language server executing.
  • Fixes a crash when generating object-orientated C code that uses inheritance
  • Fixes an issue that caused the object-orientated C generator to generate incorrect code for connections involving arrays of provided ports.
  • Fixes an issue that caused the object-orientated C generator to generate incorrect code for double-sided external components where all signals from required ports were filtered.

1.2.0-beta.5 (14/03/2022)

Improvements:

  • Verification statistics are now stored as part of the cloud verification cache, meaning that they will be available inside Eclipse even if the check was not re-executed.
  • The object-orientated C generator now generates comments that explain how to create external component implementations.
  • When verifying ports that use multiple inheritance, Coco now verifes the minimal number of ports, taking into account which ports have already been verified via a base port.
  • Coco now includes an experimental JSON output format for verification results.

Bug fixes:

  • Fixes a case where a slot could be compared for equality with another slot even if its contents were invalid.
  • Fixes a bug that caused the language-server based refactorings to incorrectly only refactor the current file, rather than all affected files in the project.
  • Fixes an issue that caused the language server to use too much memory.
  • Fixes an issue that caused the language server to report diagnostics about imports in the wrong file.
  • Fixes a crash in the language server when parsing malformed files.

1.2.0-beta.4 (07/03/2022)

Improvements

  • Pretty-printing of types within error messages has been improved to ensure that the messages are not ambiguous.
  • The language server will not permit renames to keywords or invalid identifiers.
  • The C generator now supports unique.

Bug fixes:

  • Fixes several crashes in the language server:
    • Due to a invalid modules path due to keywords or invalid identifiers being used within module paths.
    • When reloading packages shortly after a package is removed from the workspace.
    • When adding and remove packages from the workspace quickly.
    • When saving files quickly.
    • When hovering over a reference to a declaration that does not exist.
  • Fixes a crash when using an attribute that has a error.
  • Fixes SWTExceptions thrown during shutdown in Eclipse.

1.2.0-beta.3 (02/03/2022)

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.

    Warning

    The new language server is not yet fully stabilised. If you experience glitches, please restart Eclipse.

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

  • Coco now supports multiple inheritance for ports, allowing ports to extend multiple base ports. Currently this is only supported for the C++ generator, but support for C will follow.

  • Coco’s enums can now be mapped onto pre-existing enums in C or C++ using the new @mapToEnum attribute, allowing Coco-style 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 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.

  • This version includes a beta 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.

Bug fixes:

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

1.2.0-beta.2 (09/02/2022)

New features:

  • In Eclipse, rechability counterexamples are now shown as a coloured overlay on the source code, like code coverage tools.

Improvements:

  • Improved typechecking performance on very large projects, with runtimes and memory consumption reduced by up to 60%.
  • Support detection of proxy settings on RHEL6.
  • Reduce the time taken to produce large architecture diagrams both inside Eclipse and via the command line tool.
  • Improve the panning performance of the architecture diagram viewer inside Eclipse.
  • 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.
  • 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.
  • 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.

Bug fixes:

  • Further fixes to prevent Eclipse from consuming too many handles on Windows.

1.2.0-beta.1 (17/01/2022)

New features:

  • 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’s Linux release binaries are now also available for 64-bit ARM cpus (ARMV8-A or later).

Improvements:

  • The various views in Eclipse, 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 in Eclipse 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 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 highlighting on the architecture diagram has been improved to make it easier to read and to highlight more related elements.
  • 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 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.
  • The C++ generator is now able to generate code for functions that are generic over the Iterable trait.

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.