1.0 Pre-Releases

1.0.0-rc.2 (30/06/2021)

Breaking changes:

  • The previously undocumented [eclipse] section of the Coco.toml file has been removed and merged with the [generator] section. This means that:
    • eclipse.generateCodeForDependencies has been removed.
    • eclipse.outputDirectory is now generator.cpp.outputDirectory.
    • eclipse.testOutputDirectory is now generator.cpp.testOutputDirectory.
    • eclipse.codeGenerationLanguage is now generator.defaultLanguage.

New features:

  • Coco now supports three new semantically-aware transformations:

    • Flatten port: flattens a composite port into a non-composite port.
    • Merge signals: converts pairs of signals into a single signal. This is intended to merge signals that indicate success or failure into a single signal that is parameterised by the success or failure of the action.
    • Port to external functions: converts a stateless port into a collection of external functions.

  • State machines no longer have to have names, unless they are inherited from via state machine inheritance.

  • Type annotations are now optional on transitions, providing it is unambiguous which transition is being referred to. For example, the following is now allowed:

    port P {
  function f(x : Bool) : Nil
  machine {
    f(y) = {}
  }
}

  • A Coco-specific welcome page has been added to Eclipse to help first-time users login and install the example projects.

  • The state and architecture diagrams now support navigating back to the source code, and also highlight relevant elements on hover.

  • Reachability counterexamples are now shown as highlights on the state diagram.

  • External components now shutdown automatically as part of Coco’s automatic termination. This behaviour can be modified by overriding execute_unused() in the external component subclass.

  • package.testSources has been added to allow Coco files that are only used for testing purposes to be stored in the same package.

  • Code generation has improved support for complicated projects:

    • Test-related generated code (i.e. mocks or from package.testSources) can be output to a separate directory.
    • When generating code for packages that depend on other packages, generator.cpp settings are now correctly isolated per package. This means that a dependency can generate code in a different namespace from the main package.
    • Dependencies can now be regenerated as part of the main package, allowing for private copies of packages to be re-created.
    • All code generation output options can be set in the Coco.toml file, allowing teams to share common code generation settings.

Improvements:

  • PortAccess, setAccess and setUnique can now use implicit member expressions in their arguments (e.g. setAccess(r, .None).

  • Clearer diagnostics are now generated when file names clash between projects.

  • If a component has multiple provided ports, some are now allowed to be left unconnected in an encapsulating component.

  • Provided ports on encapsulating components can now be shared between a component inside the encapsulating component, and a component on the outside.

  • External components can now use setAccess to mark their required ports as shared:

    @runtime(.MultiThreaded)
external component Consumer {
  val r : Required<P>
  init() = { setAccess(r, .Shared); }
}

  • Code completion will now work more robustly when the malformed code includes an if.

  • Coco-generated mocks directly export coco_shutdown() allowing test cases to shutdown mocks if necessary.

  • The counterexample viewer now prioritises the start and ends of events when the event is too long.

  • The counterexample viewer now shows the value of single-member structs/external types inline, rather than including a redundant extra row.

  • Architecture diagrams can now be generated from the command line.

  • The assertion tree now includes icons to describe the type of element.

  • Added options to set the default directories for code generation.

  • The EMF API now includes a EMFContext.toResourceSet method to make it easier to convert an entire package into EMF.

  • Generic signatures on functions can now have defaults applied to their type parameters: e.g. function f<T1, T2 = Bool>().

Bug fixes:

  • Fixes a case where runtime errors that result from an unused() triggering an exit action were not caught by the verification.
  • Fixes a crash when parsing offer clauses with malformed guards.
  • Fixes a case where Int was prohibited from being used as the type of a parameter of a function call.
  • Fixes an internal error when verifying member functions that include nondeterminism.
  • Fixes an internal error when verifying functions that had non-verified parameters after verified parameters.
  • Fixes code completion of hierarchical imports.
  • Fixes a bug that caused the toolbars for the state and architecture diagrams to grow too large on Windows.
  • _ is now allowed inside struct literals.
  • Fixes a case where the responsiveness check for would incorrectly fail due to a multi-client performing events, starving another required port from a chance to perform its event.
  • Fixes several cases where the support-bundle command produced invalid Coco.
  • Fixes a case where an entire required port was accidentally permitted to be marked as disconnected via setAccess(.None).
  • Fixes an internal error on modules where a port and component both used the same external function.
  • Fixes an internal error when using state machine inheritance where the base state machine uses State under some circumstances.
  • Fixes EMF proxy URIs which would have resulted in the EMF models being unable to be cross-referenced correctly.
  • Fixes using the parameterised form of @eventually inside a nondet.
  • Fixes an issue where Coco keywords were permitted to be Coco module names.
  • Fixes several cases where constants defined in nested scopes could not be used as part of types.
  • Fixes a crash when viewing the architecture diagram on large components.
  • Fixes verification of models that overrode unused in a child state.
  • Fixes a case where using implicit member expressions would not work inside generic functions.
  • Fixes a case where verifying a model that used execution states and @unbounded spontaneous transitions would result in queue full errors.

1.0.0-rc.1 (20/05/2021)

This version is the first release candidate of Coco 1.0.0. This version is intended to be the final 1.0.0-compatible version of the Coco Language and no backwards-incompatible changes are now expected (unless a serious bug is encountered). See Status for more information about the status of different features.

This release includes a large number of breaking changes, and therefore there is a specific migration guide for details on how to migrate to this release candidate.

Breaking changes:

  • Coco’s syntax has been changed with the aim of reducing confusion over where ; are required or whether ‘;’ is a separator or a sequencing operator, and also improve the consistency of the language.
  • BoundedInt<l, u> has been removed in favour of Bounded<l, u-1>.
  • In order to make Coco’s integer types more safe and more consistent with a verified language, BoundedInt can no longer be implicitly converted to Int and instead requires an explicit cast.
  • The queue control functions have been renamed to improve consistency: setFilter becomes setAllow, unique becomes setUnique and setShared becomes setAccess.
  • setFilter (now called setAllow) is now variadic, meaning that setFilter(r, [s1, s2]) is now written as setFilter(r, s1, s2).
  • mutating and mutable have both been changed to mut.
  • The slot functions isValid, isInvalid, initialise and invalidate are now member functions (e.g. isValid(s) is now s.isValid()).
  • Abstracted has been removed in place of external type member variables.
  • @runtime no longer defaults to Runtime.MultiThreaded, so all components must now use @runtime.
  • @compatible has been introduced to specify which runtimes a ports should be verified in when using port inheritance.
  • The treatment of spontaneous transitions in responsiveness checking has been changed to no longer assume that they are guaranteed not to happen too quickly. A new @slow attribute has been introduced to allow certain spontaneouses to be specifically marked as occuring slowly.
  • New keywords have been reserved to allow for future enhancements.
  • Coco no longer automatically derives Default and Eq for enums, or Default for structs. Instead @derive(Default) must be added to the type declaration in order to automatically derive trait instances.

New features:

  • Coco is now able to generate an architecture diagram that shows the structure of the components in your system. This is available via the right-click menu when selecting an encapsulating component in the assertions tree. This version is only an initial release: lots of updates and improvements will follow over the next few releases, such as CLI integration.

  • Coco now has support for easy automatic termination of systems. In the generated code, components now retain a count of the number of clients connected to a provided port. When this reaches zero, the component will initiate a setNextState(Terminated) call, automatically shutting down the component. This behaviour can be overridden using the new unused transition, which allows termination to be deferred. If this is done, then the verification will verify that following the unused call, the component is guaranteed to eventually terminate. Further documentation on this will be in rc.2.

  • Implicit member expressions and patterns have been added to provide a shorter syntax for referring to members when the type is clear from the context. For example:

    function fn() : AnEnum = .X
function select() : AnEnum = nondet { .X, .Y, }
function swap(x : AnEnum) : AnEnum = match {
  .X => .Y,
  .Y => .X,
}
function fn() : Optional<Bool> = .None
function fn() : Result<Bool, Error> = .Ok(false)
@runtime(.MultiThreaded)
component C { ... }

    Implicit member expressions can be used in any place where the typechecker is able to unambiguously infer the type of the context.

  • Coco now has a new Result<T, E> type which represents the result of a function that, if it succeeds will return a value of type T, and if it fails will return a value of type E. Further, the ? operator (pronounced try operator) has been introduced to easily check and chain complex error handling code. For example:

    function execute() : Result<Bool, Error> = { fn1()?; fn2()?; return .Ok(true); }

    will execute fn1(), and if it fails it will instantly return, otherwise it will execute fn2(), again checking for failure, and it will otherwise return .Ok with the value true. See Result and Try Operator for further details.

  • Struct literals have been added to allow a struct, or external type (see below), to be allocated. For example, if Pair is defined as:

    struct Pair<L, R> {
  var left : L
  var right : R
}

    Then Pair{ first = 2, second = true } is an expression to construct the pair with the given values.

  • External types can now have a body consisting of:

    • Member variables (i.e. like structs);
    • Member external functions;
    • Static constants

    For example, the following defines

    @derive(Default)
external type Vector<T, val max : Int where 0 <= max> {
  var size_ : Bounded<0, max>
  mut external function clear() : Nil = { size_ = 0; }
  external function size() : Bounded<0, max> = size_
  mut external function pushBack(x : T) : Nil = { size_ = size_ + 1; }
  mut external function popBack() : T = { size_ = size_ - 1; }
}

    could be used to model a vector type that abstracts away from the contents of the vector and only models the size.

  • Coco’s BoundedInt type has been replaced by Bounded. This new type differs in that the upper bound is inclusive: for example, Bounded<0, 1> can be 0 or 1, whereas BoundedInt<0, 1> could only be 0. Further Bounded also includes two static constants First and Last that refer to the given lower and upper bounds respectively. For example, if type Id = Bounded<0, 5>, then Id.First would be 0 and Id.Last would be 5. First and Last can also be used in implicit member expressions: e.g. x = .Last;.

  • Instances of many traits can now be automatically derived using the new @derive attribute.

  • Attributes can now take a variable number of parameters, and all of the C and C++ attributes have been converted to being variadic. For example:

    @CPP.mapToType("std::vector<int>", CPP.ParameterStyle.ConstReference, [CPP.Header.System("vector")])

    can now be written as @CPP.mapToType("std::vector<int>", .ConstReference, .System("vector")).

  • Code completion now works in match expressions, and suggests patterns that have not yet been matched.

  • Coco can now output an index of the generated C and C++ code in JSON. This can be used to build tools that perform further generation on the results of the Coco generation. For example, the code index could be used to generate RPC or python bindings.

  • The verification is now able to identify and report spontaneous transitions that might do nothing, such as spontaneous = {}.

  • A new attribute @mustUse has been introduced to allow certain declarations to be marked as requiring use, thus prevent users from, for example, calling a function and not looking at its return value.

  • Port inheritance checks can now be performed in the single-threaded model, when using @compatible.

  • Generic parameters can now have default types specified. For example, the new Bounded type is declared as external type Bounded<val lower : T, val upper : T, T = Int>, meaning that the integer type is configurable, but defaults to Int.

  • Code completion now works inside attributes.

Bug fixes:

  • Fixes a parser bug that caused as to not have the correct binding precedence, meaning that more parentheses were required.
  • Fixes several minor bugs with the automatic formatter including with trait instances, returning external code expressions, and when mixing imports with trailing slashes.
  • Fixes an internal error caused by the typechecker erroneously using _ where a verified expression was expected.
  • Verification:
    • Fixes an internal error caused by comparing non-verified values.
    • Fixes a case where the verification would mistakently fail with a deadlock when checking for single-threaded port inheritance.
    • Fixes some cases where the responsiveness check would incorrectly pass for components with no function calls.
    • Fixes a crash when cancelling verification using the cloud service.
    • Fixes several bugs that would cause verification to incorrectly fail when a port or component had no functions calls.
    • Fixes a case where a variable initialisation of a struct member would be omitted if initialised directly via a nondet.
    • Fixes a crash when using become when passing a reference to a local variable.
  • Fixes a crash when using connect in combination with casts.
  • Fixes a case where overlapping traits would cause misleading error messages.
  • Fixes a graphical glitch in the counterexample viewer where drainQueue events would overlap.
  • Fixes a crash when clicking on certain entries in the variables pane of the counterexample viewer.
  • Fixes several cases where the simulator’s variables pane would not update as expected.

1.0.0-beta.47 (07/04/2021)

New features:

  • Events on external components are now automatically logged using the standard Coco logging functions. Specifically, calls to coco::StateMachineLogger::event_started() and coco::StateMachineLogger::event_finished() are now automatically injected at the start and end of every function call.

  • Stub subclasses are now automatically generated for external components as comments, providing an easier way to start implementing an external component. For example, given an external component like:

    @queue(Queue.Unbounded(2))
external component User {
  r : Required<Composite>;
}

    Then just after the class declaration of User, the following comment is now also auto-generated:

    /**
The following ...

\code
Header:

#include "ExternalComponents.h"

class UserImpl : public User {
  void r_sigs_pong() override;
  void r_sigs_started() override;
  void r_sigs_hasTerminated() override;
  void execute_start() override;
};
Implementation:

void UserImpl::r_sigs_pong() {}
void UserImpl::r_sigs_started() {}
void UserImpl::r_sigs_hasTerminated() {}
void UserImpl::execute_start() {}

\endcode
*/

  • ${COCO_VERSION} can now be used in generator.cpp.fileHeader, generator.cpp.headerFileHeader and generator.cpp.implementationFileHeader to inject the version of the Coco Platform used to generate the code. For example:

    [generator.cpp]
fileHeader = """
// Copyright (c) Cocotec Limited 2021
//
// Generated by Coco version ${COCO_VERSION}
"""

    would append:

    // Copyright (c) Cocotec Limited 2021
//
// Generated by Coco version 1.0.0-beta.47

    to the top of every header and implementation file.

  • When generating the Coco runtime header, the header will now generator will now respect generator.cpp.fileHeader and generator.cpp.headerFileExtension, if necessary. For example, this means that it is possible to directly generate the runtime header as coco_runtime.hpp.

  • Code generation is now more prominent in Eclipse, and a summary of the code generation and verification status is shown following completion in the Eclipse status bar.

Bug fixes:

  • Fixes an internal error and a false negative when verifying components that called functions on required ports via expressions such as e.fn() where e contains side-effects (e.g. writes to variables).
  • Fixes a case where overlapping source folders would incorrectly be allowed in package.sources.
  • Fixes several typechecker related errors when creating instances of traits including:
    • Fixes a case where where Coco would report many error messages of the form Cycles in type decls whilst declaring certain generic trait instances.
    • Fixes a case where Coco would report about type declaration cycles whilst typechecking trait instances of abstracted types.
  • Fixes a case where the generated C++ code would be incorrect if generator.cpp.fileHeader did not end in a trailing newline.
  • Fixes a case where an integer overflow caused by negating INT_MIN was not caught by the verification.
  • There is now a cap of 100 on the maximum queue size permitted during verification in order to prevent Coco from not terminating.
  • Fixes the Coco source folder overlay icon in Eclipse so that it now co-exists with other Eclipse overlay icons, suc as the problem and git status icons.

1.0.0-beta.46 (28/03/2021)

New features:

  • States are now allowed to have parameters that are not comparable for equality. States that have such parameters are not allowed to contain further nested states, and must use setNextStateReEnter instead.

Improvements:

  • Component state machines that are obviously nondeterministic and will therefore fail verification are now highlighted by the typechecker.
  • Double-clicking on a node in the assertion tree will now always do something useful, such as opening the model in the editor, or executing the verification.
  • Logging is now generated when timers are executed in the single-threaded runtime.

Bug fixes:

  • Fixes a case where using timers in the single-threaded model could result in the generated code crashing due to a queue full error.
  • Fixes crashes that could occur if verification and code generation both ran without a reload between them.
  • Fixes several verification crashes and internal errors:
    • When verifying single-threaded components with multiple provided ports.
    • When verifying components with arrays of provided ports.
    • When calling a member function on the result of another function (e.g. (x as T).fn()).
    • When verifying models that use arrays of ports in certain ways.
    • When using nondeterministic expressions as the guard in a Enum Case.
  • Fixes a bug where the pretty printer would incorrectly print member function calls.
  • Fixes a case where the pretty printer would not print the body of an external constant.
  • Fixes a case where code could not be generated if an entry action only contained a call to invalidate.
  • Fixes a case where the state diagram would be blank when using state machine inheritance.

1.0.0-beta.45 (13/03/2021)

Breaking changes:

  • Components without required ports cannot have the @queue attribute applied. These attributes can be removed.
  • Mocks are no longer generated for ports: instead mocks are only generated for external components.

New features:

  • This version includes the first release of the Coco simulator for Eclipse. This allows port and component state machines to be interactively explored, allowing the user to choose which event should be performed at each step. This release also allows a counterexample to be reopened in the simulator, allowing users to explore alternative scenarios based on a counterexample.

  • External components with required ports can have a queue:

    @queue(2)
external component C {
  req : Required<P>;
}

    The generated C++ code for C will now contain a background thread that is used to process the signals. The queue attribute can be used as normal, meaning that either bounded or unbounded queues can be generated.

  • A new header <cpp_runtime_gmock_helpers> has been added to the generated C++ code, coco/gmock_helpers.h, which contains two utility classes to ease writing gMocks. These utility classes provide methods that execute a gMock action asychronously. For example:

    EXPECT_CALL(client_mock, pinger_pong(value))
  .WillOnce(helper.InvokeAsync(Invoke(&client_mock.pinger().connected(), &PPingerProvided::terminate),
                               std::chrono::seconds(1)));

  • Attributes can now be variadic, allowing a variable number of arguments, such as attribute @attr(values... : Bool).

Improvements:

  • Eclipse:
    • Errors in the Coco.toml file are now reported more prominently by showing a red icon in the assertions viewer, rather than a blank assertions viewer.
    • Projects can be forcibly reloaded either by using Refresh in Eclipse, or by using the new refresh icon in the assertions viewer.
    • Verification can be forcibly restarted using the right-click menu.
    • The Coco tools are now installed into a version-specific directory, meaning that multiple versions of the Coco Platform can be installed side-by-side.
  • In the generated C++ code, all single-threaded components expose a coco_drain_queue() method that will drain the component’s own queue (if there is one), and then recursively drain the queue of components above it.
  • Support for additional markup fields has been added, along with translation of these into Doxygen. See Other fields for further details.

Bug fixes:

  • Fixes an error that caused the generated C++ code to be uncompilable by G++ 4.4 when using arrays of external components.
  • Fixes an internal error when attempting to verify ports using state machine inheritance where both the base and derived state machines included spontaneous transitions in the same state.
  • Fixes an issue that prevented the cloud verification icon from updating inside Eclipse.
  • Fixes an issue that would result in the cloud verification disconnecting users during long running verification jobs.
  • Fixes an error when an entry in the sources property in the Coco.toml file contains a trailing slash.
  • Fixes visibility of background_thread() method, ensuring it is private.
  • Fixes a crash when calling a member function on an external code expression.
  • Fixes a typechecker error when using the builtin definition of cast for enums several times in the same file.
  • Fixes a crash when importing EMF models that contain no embedded value in an OptionalExpr.
  • Fixes a crash when importing EMF models that contain declarations that are referenced before their declaration.

1.0.0-beta.44 (19/02/2021)

Breaking changes:

  • Variables within states must now be initialised in order. For example:

    state S {
  var x : Int = y
  var y : Int = 0
}

    is no longer permitted.

  • Variables declared at the top-level of a module must now be initialised in order.

  • Eq is no longer defined on Abstracted to prevent accidental comparisons. This means that Slot<T> can no longer be compared for equality: previously this would have compared the slots validity for equality, rather than the slot contents. In order to mark an Abstracted type as comparable for equality, use @derive. For example:

    type SequenceNumber = Abstracted<Int, BoundedInt<0, 5>>
@derive
instance Eq(SequenceNumber) {}

    This is permitted as both the original and abstracted types have an instance of Eq.

  • NonVerifiedEq and NonVerifiedOrd have been introduced to allow non-verified types to be marked as comparable for equality, and therefore be compared using == etc.

  • Return has been banned from various surprising places to ensure code clarity. For example, fn(return 0) is no longer permitted. These changes are unlikely to be noticeable by most users.

Improvements:

  • The Eclipse preferences menu now contains information about your license.

Bug fixes:

  • Fixes several issues when using encapsulating components with multi-dimensional arrays of ports and components. These would have prevented the code from compiling or would have resulted in the code crashing on startup.
  • Fixes an issue that prevented the generated code from compiling if arrays of external components were used.
  • Fixes a crash when calling a function reference with _ as an argument.
  • Fixes an internal error during verification caused by using abort() within an if expression.
  • Fixes an internal error during verification when overloading a function with multiple different non-verified types.
  • Fixes an internal error during verification when comparing an array of non-verified values.

1.0.0-beta.43 (02/02/2021)

  • Fixes a regression in 1.0.0-beta.42 which caused some EMF models to be unable to be imported.
  • Fixes a crash when verifying some components in the single-threaded runtime that used both setShared with PortAccess.Shared and also had multiple provided ports.

1.0.0-beta.42 (01/02/2021)

  • Coco models can now be exported to a native EMF representation via the EMFContext.toResource method. This effectively allows a textual .coco file to be converted into a form that EMF can natively handle, permitting Coco models to be further transformed using other tools in the EMF ecosystem. See EMF for further details.
  • As part of our goal of stabilising Coco for version 1.0, this release contains several backwards-incompatible changes that will now cause some Coco scripts to be rejected:
    • Function calls where multiple overlapping references are passed to a single function are now prohibited: e.g. f(&x, &x) is now prohibited.
    • External functions must now write to all parameters of type &out T. If the type is non-verified, then _ can be used as the value (e.g. x = _).
    • External functions must now always have a body, specifying the verification side-effects of the function.
    • External constants must now always have a value.
    • Arrays are now always verified. Previously, a variable of type Array<T, k> where T is non-verified would not be verified, meaning that array accesses such as x[i] would not always be checked potentially meaning that i could be out-of-bounds in the generated code. This is no longer the case, and arrays are now treated as verified whether their element type is verified or not.

Bug fixes:

  • Fixes an issue that would cause components using setShared with PortAccess.SignalOnly not to give the correct verification results.
  • Fixes an issue when verifying components with multiple ports where the ports had fields.
  • Fixes an issue that would cause verification-relevant side-effects on non-verified variables to be incorrectly omitted.
  • Fixes several internal errors that would be reported when verifying models using string literals.
  • Fixes a bug that prevented final from being specified on a port that itself inherits from another port.
  • Fixes an error that prevented C++ from being generated when components have multiple provided ports.
  • Fixes several warnings reported by gcc in the C++ runtime header.

1.0.0-beta.41 (14/01/2021)

  • The Coco Platform now includes a .NET-compatible API available as a NuGet package.
  • All jars and Windows binaries are code signed using an EV code signing certificate.
  • Coco:
    • Generic functions that contain nondeterminism are now prohibited, since they are not supported by the verification at the moment.
    • Composite ports that contain a field of type f : P where P is also a port with a state machine are now prohibited.
    • Implicit conversions from values of type T to &T are now prohibited.
    • Adds a warning when a signal is constructed but not sent and used as a statement.
    • Fix an error message when parsing TOML files.
  • C++:
    • Fixes a crash in the generated code when an encapsulating component has a required port that is internally connected to several components.
    • Fix some issues that prevented the generated code from compiling when combining state machine inheritance and encapsulating components.
    • Fixes an issue that prevented the generated code from compiling when a component has an array of required composite ports.
  • Verification:
    • Fixes a case where required ports were not allowed to send signals on startup, leading to some models erroneously passing verification.
    • Fixed some cases where a value of type Slot<T> would not be checked for validity before being passed to a parameter of type &T.
    • Fixes several internal errors that could occur when verifying ports that use state machine inheritance.
    • Fixes an internal error raised when models were forcibly reverified.

1.0.0-beta.40 (15/12/2020)

  • Restores the previous C++ generator behaviour, where each port maps to three classes.
  • Fixes an issue when using generator.cpp.headerOnlyPorts that would have prevented the generated C++ code from compiling.

1.0.0-beta.39 (14/12/2020)

  • Fixes an issue when using the Coco EMF frontend that would prevent MemberReferenceExpr from being used under certain conditions.

1.0.0-beta.38 (12/12/2020)

  • C++: the C++ generator has undergone a major rewrite to improve the quality of the output, fix various issues, and provide more flexibility for future enhancements.
    • gMock-compatible mocks can now be generated for external components.
    • Encapsulating components now check that instances of all external components have been provided before starting to avoid hard-to-debug errors.
    • Encapsulating components now block in their destructor waiting for all internal components to terminate. This makes it easier to ensure clean termination.
    • External components now include more helpful methods to easily send signals to subscribers.
    • Subscribers can now completely deregister themselves from receiving signals from a component after startup.
    • Improved the representation of single-threaded subscribers so that component’s now hold a list of single-threaded components, rather than single-threaded ports. This will improve performance on large models.
    • Improve the doxygen output in several cases.
    • Char literals can now be generated.
    • virtual functions are no longer marked as inline.
    • Names of all Coco-defined runtime variables are now mangled to a consistent style.
    • Added an option generator.cpp.flatFileHierarchy that outputs all files in a single directory.
    • Fixes several issues where the generated code for external components could not be compiled.
    • Fixes an issue with include guard printing which would have caused errors when compiling the generated C++ code.
    • Fixes a bug in the generation of != that would cause it to erroneously return true.
    • The single-threaded generator no longer uses std::atomic.
  • C:
    • This version includes an alpha version of the C generator for testing by selected users. If you would like to try the C generator, please contact support@cocotec.io.
  • Coco:
    • Allow Optional<T> to be considered as a verified type even when T is non-verified. In this case, the verification will only store whether the Optional has a value or not, rather than storing the concrete value.
    • External components can now have either have required ports or provided ports.
    • The typechecker now produces an error when patterns in a match overlap.
    • Components can now have arrays of provided ports. This is equivalent to having multiple provided ports, but has the convenience of having a single array.
    • NonVerified<T> is now defaultable.
    • Fixes a case where explicit integer values could erroneously be assigned to tagged enum cases.
    • Fixes a case where nested for loops would sometimes loop infinitely.
    • Fixes an issue where guards on arrays were erroneously allowed to have side effects.
    • Fixes a case where @eventually was ignored when used on a optional expression.
    • Fixes a crash when verifying some modules that use the String type.
    • Fixes a crash when verifying models that include expressions such as (x = y).fn().
    • Fixes a crash when using match on values of type State.
    • Fixes a crash when verifying models that use Slot<T> on an out parameter.
  • Documentation:
  • Eclipse:
    • The state diagram viewer has been re-written to integrate better into Eclipse, and has now been re-enabled on Linux.
    • Rendering performance of the state diagram has been improved.
    • If a check results in both a verification warning and error, priority is now given to the error.
    • Fixes a case where the counterexample viewer could not display values stored in nested structs.
    • Fixes a resource leak when using the counterexample viewer for long periods of time that caused an error like No more handles.
    • Fixes a display artefact on Linux where the lifeline header would appear next in the scrollbars.

1.0.0-beta.37 (24/10/2020)

Breaking changes:

  • If x is a variable is of type &T, then it is no longer necessary to write &x when passing. For example, given:

    function f(x : &out Int) : Nil = ...

    then it is no longer necessary to write f(&x) and instead f(x) is permitted. The typechecker will generate a warning and fixit in this release, but this will be removed in a subsequent release.

Improvements:

  • The counterexample viewer has been improved and should be more compatible with Eclipse, particularly on Linux. This release also resolves various crashes and other graphical glitches that have occurred when viewing counterexamples on Linux.

  • The state diagram viewer has had several enhancements to improve its accuracy on entry actions and calls to setNextStateReEnter. Further, spontaneous transitions and the initial state are now represented graphically, and edge labels will no longer contain duplicate names when collapsing multiple edges.

  • Added an automatic fixit when the typechecker detects that a user meant to write P.sig instead of sig.

  • Arguments can now be passed by an immutable reference. For example:

    function f(x : &Int) : Nil = ...

    represents a function that takes a reference to an immutable Int.

  • self is now of type &T or &mutable T depending on whether the enclosing function is mutating.

Bugfixes:

  • Fixes several cases where diagnostics would be missing when mounting projects on Windows are located on DFS volumes, or with very long paths.
  • Fixes syntax highlighting of &mutable.
  • Fixes a case where the automatic formatter would insert & to a newline.
  • Fixes a crash that could have resulted when executing C++ generated from encapsulating components with required ports where part of the required port is marked as unused (i.e. using setShared).
  • Fixes a case where extra semicolons were erroneously allowed.
  • Fixes a case where calling a mutable member function on an object after calling an immutable member function would give a typechecker error.
  • Fixes an error that caused incorrect verification results when using for loops inside execution states.

1.0.0-beta.36 (08/10/2020)

Breaking changes:

  • The syntax for denoting reference types has changed from out T or inout T to &out T and &mutable T, respectively. The tools will continue to accept both old and new versions of the syntax and will produce fixits for the old version. Support for the old syntax will be removed in a future release.
  • The generator.cpp.cocoRuntimeHeaderPath option has been renamed to generator.cpp.cocoRuntimeHeaderPrefix, and now indicates a custom prefix to use, rather than a custom path.

Improvements:

  • Added a new command, support-bundle, to the coco command line tool that bundles up all files required to load a project in an obfuscated form in order to send to support. This command is designed to be used in cases where the full model cannot be sent as it is sensitive, and so all names and strings are automatically obfuscated, and all comments in the model are removed.
  • Coco is now distributed as a statically-linked binary on Windows, meaning that the Visual Studio C++ runtime no longer needs to be installed.
  • Counterexamples that result from a match clause not matching now give the value that did not match directly inside the error message.
  • Counterexamples to the Usability assertion for a port can be suppressed by adding @ignoreWarning(Warning.Usability) to a port state machine.
  • Improves ranking of code completion results in Eclipse, in order to prioritise matches that include the characters consecutively.
  • Added some documentation on using the state diagram viewer.

Bugfixes:

  • Fixes a crash when using code completion on syntactically invalid member functions inside structs or enums.
  • Fixes a case where signals received from arrays of required ports would not match any transitions.
  • Fixes the combination of --output-runtime-header=true and the use of cocoRuntimeHeaderPath, and coco will now output the runtime headers to be specified custom path.
  • Fixes a case where Eclipse will show the old contents of a previously-deleted file when a new file is created on disk.
  • Fixes a crash when calling range with more complex arguments.
  • Fixes a crash when a value of type Range is included in a counterexample.
  • Fixes a case where diagnostics would disappear in Eclipse after running verification or code generation.
  • Fixes reporting of diagnostics created when generating C++ inside Eclipse, which previously caused large parts of the document to be highlighted.
  • Fixes an issue that prevent the Coco plugin for Eclipse from loading projects that were mounted on DFS volumes on Windows.
  • Fixes an issue that caused Coco to run out of memory when typchecking encapsulating components with large numbers of child components.
  • Fixes a case where double-clicking on the assertion tree would open the file, rather than the counterexample viewer.

1.0.0-beta.35 (16/09/2020)

  • Fixes a crash when become is the common successor of many different function calls.
  • Fixes a crash when using function references as signal arguments.
  • Fixes a case where the Eclipse editor would delete part of the text when formatting large documents.
  • Fixes the icon shown when user errors occur during verification.
  • Fixes an issue that caused the license server to create lots of zombie processes.
  • Fixes a case where the license server could not connect if proxy settings were specified.
  • Fixes an issue that prevented the assertions tree from being refreshed if Convert to Coco Project was used.
  • Improve counterexamples when verifying single-threaded components that have multiple provided ports.
  • Increase the limit on the number of diagnostics reported inside Eclipse from a single project.
  • String literals are now properly escaped in generated C++ code.

1.0.0-beta.34 (07/09/2020)

  • Fixes a crash when typechecking models that include invalid parameter types under certain circumstances.
  • Fixes a crash when setting referenceKind = ReferenceKind.IN_OUT via the EMF integration.

1.0.0-beta.33 (04/09/2020)

  • New features:

    • Eclipse and coco now include a state diagram visualiser that allows you to visualise Coco state machines graphically. The visualiser preserves the hierarchical states of the original Coco state machine. This is an initial release of this feature, and more improvements will be made over the upcoming releases.
    • This documentation has been rethemed to match the rest of the website, and now includes enhanced search features.
    • Coco now has support for storing references to functions in variables. For example, var x : Optional<(Bool) -> Nil> denotes a variable x that can optionally store a function that takes a Bool and returns Nil.

  • Breaking changes:

    • The syntax for specifying in, out and inout parameters has been changed to move the label next to the type, rather than next to the identifier. Further, the in keyword has been removed. For example, the following function:

      function old(in x : Bool, out y : Bool, inout z : Bool) : Nil

      is now written as:

      function new(x : Bool, y : out Bool, z : inout Bool) : Nil

      The compiler currently accepts both the old and new syntax, and generates warnings and fixits if the old syntax is used. Support for the old syntax will be removed in the next beta.

    • The syntax for denoting reference types has changed from &T to either out T or inout T, depending on what sort of reference is required.

  • Improvements:

    • The assertions tree in Eclipse has been updated to include more accurate icons, and make more status information available via the tooltip.
    • Diagnostics are now created in Eclipse whenever verification fails, allowing the problems view to act as an overview of all syntactic or verification issues in the project.
    • Documentation for the Coco plugin for Eclipse is now available.
    • Errors when connecting to remote verification service are now reported in both Eclipse and via coco.
    • A warning is now generated if an enum with just a single member is used.
    • .. is now permitted in package.sources.
    • Counterexamples that involve more than one function call to a port containing an @unbounded spontaneous transition have been improved to give both function calls.
    • Improved verification of models with @unbounded spontaneous transitions to remove some false failures.
    • Type classes have been renamed to traits.
    • Extra command line options have been added to coco to allow the most important output-related options to be configured directly.

  • Bug fixes:

    • Coco:
      • Fixes an issue that caused some complex binary operator expressions such as 10 - 2 * 3 + 4 to be bracketed incorrectly.
      • Optional<T> is now defaultable even if T is not.
      • Member functions on structs and enums no longer cause spurious typechecker errors if used in a different order to declaration order.
      • Fixes an issue that caused code completion on unique to generate results that would be type-incorrect if selected.
      • Fixes an issue that would have led to spurious warnings about state machine variables being unused if they were used before their declaration.
      • Fix a crash when parsing malformed mutating function declarations.
    • C++:
      • Fixes an syntax error when generating code for custom instances of Eq and Ord classes defined on generic types.
      • Generic enums and records are now always passed by const-reference.
      • Fixes an issue that prevented using abort inside member functions of enums or structs nested in ports.
      • Fixes a crash when generating code with no field members, but with function members.
    • Eclipse:
      • Fixes several related issues that would have caused odd behaviour in the text editor, including formatting resulting in corrupted buffers, diagnostics that would never disappear, diagnostics appearing at the wrong location, and other general stability issues.
      • Fixes an issue that would cause diagnostics to never be removed when a file imported another file that had a warning, but was otherwise error and warning free.
      • Fixes an issue that mean the assertions tree would be blank if a project was reopened without restarting Eclipse.
      • When a file is deleted and then recreated, the correct version is now displayed.
      • The plugin now automatically reloads projects that are stored on NFS filesystems when changes are made locally.
    • Command-line tools:
      • An error is now given if coco --restrict is used, but the file is not recognised.

1.0.0-beta.32 (24/07/2020)

  • The error message displayed when the maximum number of @eventually attributes is exceeded has been improved to quantify how many attributes are permitted, and how many are currently in use.
  • The error message displayed when multiple functions calls are made consecutively to a port with @unbounded spontaneous transitions has been improved.
  • Several minor improvements have been made to C++ code:
    • Calling abort from within a state machine will now send a message to attached StateMachineLogger, if there is one.
    • Fixes a case where names of instance variables would be unnecessarily qualified.
    • Improves the naming of the setNextState functions in the generated code, removing the suffix 0 that would sometimes be appended.
  • Fixes several issues with the generated C++ code:
    • Fixes a case where generator.cpp.cocoRuntimeHeaderPrefix was ignored.
    • Fixes some warnings about implicit conversions between signed and unsigned integers.
    • Fixes a case where include statements could be duplicated in the generated C++ code.
    • Fixes a case where a type would be both forward-declared, and also included.
  • Fixes an issue that would prevent Signal from being used in combination with port inheritance under certain circumstances.
  • Fixes a crash that occurred when verifying a model that stored a struct in a Optional.
  • Fixes a case where the verification would flag a component as deadlocking when using setShared in single-threaded components.
  • Fixes a case where the body of Eq would be required when verifying a model that used a variable of type Abstracted.
  • Fixes an issue where deps files were placed in the wrong directory.
  • Fixes an issue where deps files were generated even when -restrict was specified.
  • Fixes an issue where multiple copies of Signal were suggested during code completion.

1.0.0-beta.31 (12/07/2020)

  • New features:

    • Enums and structs are now allowed to have member functions. For example

      struct Buffer<T> {
  data : Array<T, 2>;
  size : Int;

  function isEmpty() : Bool = size == 0
}

    • A new type Optional<T> has been added to the standard library, providing a convenient way of handling data that may or may not be present. This translates to std::optional if C++17 or greater is being targeted for code generation, or a custom-defined coco::optional type if not.

    • A new type Signal has been added to represent a signal that has been given its parameters, but has not yet been sent. This allows code to be parametrised by a signal to send, and even permits signals to be passed via function calls. For example:

      port P {
  function sendMeS2() : Nil
  function sendMe(sig : Signal) : Nil

  outgoing signal s1(x : Bool)
  outgoing signal s2()

  machine M {
    state Idle {
      sendMeS2() = setNextState(Send(P.s2()))
      sendMe(sig : Signal) = setNextState(Send(sig))
    }
    state Send(toSend : Signal) {
      spontaneous = {
        send(toSend);
        setNextState(Idle);
      }
    }
  }
}

      Note the use of P.s2() to create an instance of Signal, rather than s2() which would immediately send the signal to P’s client.

    • The typechecker will now warn about unused variables, or variables that are declared as being mutable but could have been declared as immutable constants.

  • Breaking changes:

    • send is now a reserved function name within a port.
    • Signal has been renamed to AnySignal.

  • Improvements:

    • The connection status to the remote verification server is now shown in the Eclipse toolbar, if it is in use.
    • Encapsulating components are now validated to ensure that they are acyclic: that is they do not connect a required port of a component to a provided port that will ultimately link back to the original component.
    • Eq is now automatically derived even for generic enums.
    • Default and Eq are now automatically derived even for generic enums with generic requirements.
    • Improved typechecking of symbolic generic constraints so that, for example, x <= y is automatically inferred if x < y is already known.
    • Symbolic generics, such as struct S <val ub : Int> { value : BoundedInt<0, ub>; } can now be verified.
    • C++:
      • The C++ generator will now create templated C++ declarations for generic Coco declarations.
      • Improved C++ handling of Default, which is now mapped onto calls to C++’s default constructors.
      • The representation of tagged enums has been improved and they now use std::variant if C++17 or greater is being targeted for code generation, or a custom-defined coco::variant type if not.
      • Added an option generator.cpp.outputRuntimeHeader that controls whether the coco/runtime.h header should be output as part of the code generation. This is also available via the command-line tooling as --output-runtime-header.
      • The C++ runtime header has been simplified when targeting G++4.4.
      • Improved the readability of the C++ generator by converting switch into if wherever it is simpler to do so.

  • Bug fixes:

    • The Enabled (remote when available) option will now correctly query the verification results cache on load.
    • Fixes a case where the queue contents could become corrupted when verifying models that used @unbounded.
    • Fixes a case where a variable of type Slot<T> was not being checked for being valid before being passed to a function with an inout parameter of type T.
    • Fixes a case where components with no provided ports were incorrectly flagged as being deadlock free.
    • Fixes a case where the array index was not checked for being an integer.
    • Fixed a rare crash when verifying ports or component with multiple errors at the same level of the search.
    • Fixed a crash when verifying models that used Char.
    • Fixes verification of models that read an out parameter that had been previously written to.
    • Fixes a crash when verifying state machines that included calls on arrays of required ports with more elaborate array indices.
    • Fixes a crash when using ! in an argument to a function called on a required port.
    • Fixes a crash when creating an argument of type State to a state.
    • Fixes a scoping error that prevent integer constants defined within state machines from being used as arguments to generic types.
    • Fixes an issue that prevented setFilter from being used from EMF models.

1.0.0-beta.30 (09/06/2020)

  • Fixes a problem that prevented Eclipse from loading the Coco Platform on Windows.

1.0.0-beta.29 (08/06/2020)

  • New features:

    • Implementation components are now permitted to have multiple provided ports. The verification will check that the component implements each of the ports independently.

    • A new expression, optional has been added to allow a more concise representation of optional behaviour when defining ports. For example, the following defines a function that nondeterministically emits a signal, or does nothing:

      maybeSend() = optional sig()

    • Verification of single-threaded components that share required ports (via setShared) has been enhanced to enforce the fact that for any required port, between any two idle points the port may only send signals to one client. As part of this, setShared cannot be called on single-threaded required ports with PortAccess.Shared or PortAccess.SignalOnly.

  • Improvements:

    • The verification will now return shorter counterexamples to responsiveness checks in many cases. This should be particularly noticeable on more complex models with many required ports.
    • The typechecker now enforces the fact that _ should be used as the return value of external functions or event transitions in port state machines if the return type is non-Verified. This is to ensure it is clear what is verified and what is not.
    • The typechecker now gives errors when Abstracted or non-Verified types are used in ports or external functions. As above, this ensures that users are aware that using such types in ports or external functions would not be verified at all.
    • Components with no provided ports are now permitted.
    • Array dereferencing now respects the non-verified status of the array and index. For example, if a is of type Array<Int, 2>, then a[i] will now return something of type NonVerified<Int> if either a is non-verified, or if i is of type NonVerified<Int>.

  • Bug fixes:

    • Fixes a case where the typechecker would incorrectly compute the runtime of required ports in arrays, thereby allowing some architectures to be allowed when they should have been rejected.
    • Fixes a case where the typechecker would erroneously accept scripts that implicitly converted &Slot<T> into Slot<T>.
    • Fixes a case where the responsiveness check would erroneously pass if the entry() action of Main started a non-responsive loop.
    • Fixes a crash when verifying or generating C++ code on models that included a reference to a signal without calling it.
    • Fixes a rare case where the verification could produce incomplete counterexamples that would show the provided port as only being able to perform a subset of the signals that it could actually perform.
    • Fixes a case where an internal errors were reported when using non-verified state parameters.
    • Fixes a case where internal errors were reported when using functions that had multiple non-verified arguments.
    • Fixes several cases where using out parameters in functions defined in state machines that communicated would lead to internal errors.
    • Fixes a case where verification results would not be loaded from the cache if there was event a single model with syntax errors.
    • Fixes a case where the new module dialog in Eclipse would be blank.
    • Fixes a crash that occurred when generating C++ code for encapsulating components that uses the mixed runtime with arrays of required ports.
    • Fixes a warning in the C++ runtime header about comparing unsigned and signed types.

1.0.0-beta.28 (08/05/2020)

  • New features:
    • The Coco Platform now includes a cloud verification service, which is now launching in alpha form. In addition to performing all verification work remotely, this service also provides a cache meaning that the Coco plugin for Eclipse will instantly load verification results if a project that has been previously verified is opened. To enable this service for your account please contact support@cocotec.io.
  • Improvements:
    • The Coco Tutorial has been extensively updated.
    • &&, || and ! now correctly preserve the non-verifiedness of their arguments; i.e. if any of the inputs to one of the previous operators is non-verified, then so is the result.
    • The typechecker now rejects functions that use return _; (or equivalents) when the function has a verified return type. Previously this error was only caught when running the verification.
    • External code expressions are now required to be of non-verified types.
    • Code completion now suggests import kinds such as unqualified.
    • Added a warning when a user creates an array of type Array<NonVerified<T, k>> indicating that NonVerified<Array<T, k>> is more efficient.
    • Auto-detection of proxies is now supported on Linux, as is connecting via authenticated HTTP Connect proxies.
  • Bug fixes:
    • Fixes a case where Eclipse would sometimes show out-of-date diagnostics for previous versions of the file.
    • Fixes a case where the code completion would insert the function parameters again, resulting in repeated parameter lists.
    • Fixes incorrect diagnostics being generated when loading a Coco model using EMF.
    • Fixed the automatically generated fixits that involve Slot, Provided and Required.
    • Fixes a crash when generating code using Slot.
    • Fixes a rare crash that could occur when typechecking uses of generic functions that have only a single overload.

1.0.0-beta.27 (19/04/2020)

  • Breaking changes:
    • The contents of the SlotAbstraction module has been moved into Base, meaning that import SlotAbstraction is no longer required.
    • The @verify attribute has been removed.
  • New features:
    • Ports can be declared as final to prevent them being inherited by another port.
    • Types are no longer required to always have a default value, which makes it possible to correctly model native types that do not have well-defined default values, such as C++ types that do not have default constructors. Types that are defaultable have to conform to the Default trait.
    • Improved support for marking types as verified:
      • External types are always marked as non-verifiable.
      • Coco primitive types are always marked as verifiable, as are enums and structs that contain verifiable values.
      • NonVerified can be used to obtain a non-verified version of a verified type; e.g. NonVerified<Int>.
      • A new trait Verified can be used to determine if a type is verified.
    • Slot can now be used inside structs, enums, and as an argument to a generic type (e.g. Array<Slot<T>>).
    • Slot can now be assigned to from a value of type T providing !Verified<T>.
    • Added support for connect statements from a required port of type P and a provided port of type Q where Q inherits from P (i.e. Q <: P).
    • Generic requirements can now:
      • Compare integer values (e.g. function fn<val x : Int, val y : Int where x <= y>).
      • Compare types for equality (e.g. function fn<S, T where S == T>).
      • Compare types for subtyping (e.g. function fn<S, T where S <: T>).
      • Negate requirements for comparisons (e.g. function fn<S, T where !(S <: T)>.
      • Negate requirements that a type is verified (e.g. function fn<T where !Verified<T>>.
  • Improvements:
    • Declaring an Array of negative size now gives a typechecker error.
    • Declaring a BoundedInt where the lower bound is greater than the upper bound now gives a typechecker error.
    • Mismatches in types between BoundedInt and Int between ports and components will now be caught.
    • Counterexamples that involve Slot will now be easier to read.
  • Bug fixes:
    • The Eclipse assertions tree now correctly marks files as containing errors if diagnostics are only found when generating code or running verification.
    • Fixes a case when using setShared and unique in a component without importing the module containing those ports would fail.
    • Fixes a case when verification would give incorrect results when using a port of type T as both a required port, and inside an array of required ports.
    • Fixes a case when verification would incorrectly fail with a responsiveness error when using multiple required ports that use @unbounded.
    • Fixes a crash when using the Coco editor, and incorrectly using a function involving Slot.
    • Fixes a case where the generated C++ code had warnings about assignments inside ifs.
    • Fixes a crash when a declaration marked with @CPP.ignore was required for code generation.
    • Fixes several edge cases where side-effects that could impact verification but were on non-verified function arguments were ignored.
    • Fixes a case where the generated C++ code would select the wrong transition to fire when using hierarchical states with guards.
    • C++ code can now be generated for ports that contain external types.

1.0.0-beta.26 (18/03/2020)

  • New features:
    • Out parameters can now be read from, providing that they have been written to first. The compiler will now also check that out parameters are always written to before the end of the function; previously this was only a warning.
    • Diagnostic notes are now shown in Eclipse, making it easier to track down some errors.
    • coco --diagnostic-format can now be used to output diagnostics in machine readable formats. For example, coco --diagnostic-format=checkstyle-xml typecheck will make coco output Checkstyle-compatible xml, as accepted by many other tools.
    • Eclipse now supports setting a specific folder as the exclusive Coco source folder, in addition to the previous options of adding and removing folders as Coco source folders.
  • Bug fixes:
    • External code expressions can now be used in assignment expressions where the variable is abstracted.
    • setShared can now be called on fields of base ports through derived instances.
    • Fixes a bug where the output of coco verify --format=junit would generate invalid XML due to invalid escape sequences.
    • Fixes an issue where derived ports would erroneously pass verification.
    • The deprecated Eclipse navigator view has now been removed from the Coco perspective.
    • Fixes several issues that led to unclear counterexamples between base and derived ports.
    • Fixes an issue where new port and component declarations would appear in the wrong order in the assertion tree viewer.

1.0.0-beta.25 (01/03/2020)

  • Breaking changes:

    • Single-threaded encapsulating components must now be specified using @runtime(Runtime.SingleThreaded).

  • New features:

    • Adds support for mixing the single-threaded and multi-threaded runtimes. An encapsulating component labelled with @runtime(Runtime.MultiThreaded) and that contains single-threaded components will automatically generate appropriate wrapper code to guarantee that the locking is safe. Required ports of single-threaded components can also be labelled by @runtime(Runtime.MultiThreaded), which allows them to be connected to multi-threaded components, and will ensure that the verification verifies this is sound.

    • Allows ports to inherit from other ports:

      port PBase {
  function start() : Nil
}

port PDerived : PBase {
  function start(p : Bool) : Nil
}

    • Allows port state machines to inherit from other port state machines:

      port PBase {
  function start() : Nil
  machine MBase {
    state Start {
      start() = {}
    }
  }
}

port PDerived : PBase {
  function start(p : Bool) : Nil
  machine MDerived : MBase {
    state Start {
      start(p : Bool) = {}
    }
  }
}

  • Bug fixes:

    • Fixes a crash when generating C++ on state machines using purge in exit actions.

1.0.0-beta.24 (04/02/2020)

  • Bug fixes:
    • Fixes an issue that would reduce the verification results cache hit rate.
    • Fixes a crash when using @unbounded with a queue size of 0.
    • Fixes an issue where some malformed models that use @unbounded together with entry and exit actions would be mistakenly accepted.
    • Fixes an issue where setNextState was mistakenly permitted in @unbounded transitions.
    • Fixes a crash when using @unbounded in state machines with no other transitions.

1.0.0-beta.23 (28/01/2020)

  • New features:
    • Adds C++ code generation support for:
      • Components that require arrays of ports.
      • Models that contain user-defined instances of Eq and Ord.
    • Declaration statements for unverified variables can now be initialised as per normal variables.
    • Assignment expressions involving non-verified variables can now be chained (e.g. x = y = z).
  • Bug fixes:
    • The typechecker now checks that models only use return _; in external functions and ports.
    • Fixes a bug that caused the generated C++ code not to compile when log was used as an expression.
    • Fixes an issue where the verification would report a deadlock when using the single-threaded runtime with multi-client models.
    • Fixes an issue where the verification would report a deadlock when using @unbounded with multi-client models.
    • Fixes a rare crash that would occur on startup on Windows.
    • Fixes a crash when cancelling verification on large projects.
    • Fixes a crash that could occur during verification.

1.0.0-beta.22 (05/12/2019)

  • Adds debugging information to the provided port when the implements its provided port check check fails.
  • Fixes an issue where code completion would not work on unique.
  • Fixes an issue where verifying @eventually properties on components with multi-client required ports could erroneously fail.
  • Fixes an issue that would prevent custom instances of Cast from being created.

1.0.0-beta.21 (28/11/2019)

  • Adds an attribute @CPP.include to add additional includes when a declaration is generated.
  • Adds an attribute @CPP.identity to indicate that a function is the identity function and can therefore be suppressed when generating code.
  • Fixes a case where MSVC would be unable to compile the generated C++ code with a queue size of 0.
  • Fixes a crash when using unsubscribe in combination with setShared and PortAccess.OtherOnly.

1.0.0-beta.20 (25/11/2019)

  • Fixes a crash when using @unbounded when there is no queue.
  • Improves compatability with G++4.4.

1.0.0-beta.19 (25/11/2019)

  • Fixes a crash when using purge when there is no queue.
  • Adds runtimeAssert and runtimeAbort which only create assertions in generated code, rather than in the CSM code.
  • Added further gmock generation for provided ports.

1.0.0-beta.18 (18/11/2019)

  • Breaking changes:

    • @eventually has been altered to ensure it is consistent between nondet, offer and spontaneous.

  • Improvements:

    • Port state machines can now directly manipulate the abstracted version of a type; i.e. if a port state machine contains a variable of type Abstracted<From, To>, the port state machine can now behave like an external function and manipulate the variable as though it was of type To.

    • Improved verification performance on Windows on large projects by between a factor of two and four, particularly on large multicore machines.

    • Allow illegal to occur as the case of an offer:

      offer {
  if (b) illegal;
  if (!b) ...;
}

    • The C++ generator is now able to raise diagnostics before code is generated if names will clash in the generated code.

    • Errors are now raised whenever attributes are duplicated.

    • Improved Eclipse performance on large projects.

    • Allowed nondet expression to occur within an @unbounded declaration.

    • Added fixits when mixing up nil and Nil, or when incorrectly typing the types of parameters in state machines.

    • Improved the error messages generated when the type of parameter (i.e out, inout etc) does not match between a function declaration, and its use in a state machine.

  • Bug fixes:

    • Fixed @verify when used on out or inout parameters.
    • Diagnostics are now created if either a filename is invalid, or when the source folder declaration in the Coco.toml file is incorrect.
    • Fix code completion where asking for completions after sp could result in spspontaneous.
    • Fixes an internal error when verifying enums that contain non-verified arguments.
    • Allow _ to be used as an argument to an enum constructor.
    • Fixes an error that resulted in the assertion tree going blank within Eclipse.
    • Fixes a null-pointer exception that occured when saving a file with no .coco extension.
    • Improves diagnostics in the case that imports clash.
    • Fixes code completion when importing declarations from sub-folders.
    • Removes destructor calls to primitive types in the generated C++ code.
    • Fixes an error that prevented the generated C++ code from compiling when out parameters were used.
    • Fixes an error in the generated C++ code when components with large numbers of signals are generated.

1.0.0-beta.17 (19/10/2019)

  • Breaking changes:

    • @queueSize has been renamed to @queue.

  • New features and improvements:

    • @unbounded can be specified on spontaneous transitions to indicate that the spontaneous transition may produce an unbounded sequence of signals to the component above. This will allow the verification to continue but without the usual queue full error. In return, @unbounded transitions are subject to several restrictions, most notably they must be at the top-level of a state machine. @unbounded can also take a parameter to indicate when the signal is guaranteed. Note that this is a preliminary release of this, and it is subject to change.

    • @queue now supports unbounded queues at runtime; @queue(Queue.Unbounded(x)) means that at runtime an unbounded queue should be used, but at verification-time a queue of size x should be used. This is intended to be used with @unbounded. The C++ generator has also been updated (along with the C++ runtime) to include support for unbounded queues, which use std::queue underneath.

    • Improved performance when verifying very large models, with savings of up to a factor of 10 on peak memory consumption and time.

    • @unreliable and @eventually now take optional boolean arguments that specify when they apply. For example:

      @unreliable(!request)
spontaneous = { reply(); }

      The above indicates that a the signal reply() is only unreliable when request is false.

    • Attributes can now be overloaded based on the number of arguments.

    • Added an option in the Coco.toml generator.cpp section called allowSpuriousDrainQueue that makes the generated C++ code for single-threaded models more robust by allowing coco_drain_queue to be called even in the middle of an active function call.

    • Added an option in the Coco.toml language section called disabledWarnings that disables warnings produced by the compiler:

      [language]
disabledWarnings = ["Unreachable"]

      The above disables all warnings about unreachable code.

    • Improved performance on very large models in Eclipse.

    • Improved the formatting of else-if.

  • Bug fixes:

    • Fixes a crash that occured when using purge() in local functions.
    • Fixes loading very large projects in Eclipse that contain large numbers of warnings.
    • Fixes a crash when generating C++ code for encapsulating components with required ports.
    • Fixes a crash that occured when resolving counterexamples when finding a queue full error in models using filters.
    • Fixes a bug when using @eventually on spontaneous transitions in a parent state.
    • Fixes a crash when typechecking an encapsulating component with missing connections.

1.0.0-beta.16 (03/10/2019)

  • Fixes an issue where generated C++ code within namespaces was not sorted according to a valid declaration order.
  • Adds an option to generate header-only port implementations.
  • Fixes a bug where external code expressions were rejected in signal arguments.
  • Fixes a bug where isValid and isInvalid were included in the generated C++ code.

1.0.0-beta.15 (02/10/2019)

  • Fixes an issue where code generation could crash on heavily recursive definitions.

1.0.0-beta.14 (01/10/2019)

  • Fixes an issue where long strings were reformatted to invalid multiline string literals.
  • Fixes an issue where models using abstraction gave internal errors.
  • Fixes an issue where invalid code would be generated for parameterised states.

1.0.0-beta.13 (30/09/2019)

  • Fixes an issue where offer clauses would be pretty-printed with extra semicolons.

1.0.0-beta.12 (27/09/2019)

  • Major improvements to code completion:
    • Code completion for setNextState should give much better results with better ranking of results. Further, parameters are now automatically completed when typing the name of a parameterised state.
    • Code completion after ‘:’ should be much more relevant with better ranking of most useful results, particularly when giving the type of a provided or required port.
    • Improves filtering of code completion results after a few characters are typed.
  • C++ generator:
    • Ensures that structs and complex enums will be passed by const-reference wherever possible.
    • Adds a compatability mode for the C++ generator to generate code compatible with G++4.4
    • Improves the C++ runtime to ensure code generated for older compilers is forwards-compatible.
    • Preserve statement-level comments in the Coco file into the generated C++ code.
  • Coco:
    • Adds a function log(msg : String) that can be used in a component to send a message via the state machine logging framework.
    • Defaults @queue to 0 if not provided.
    • Defaults @verify to false on external types.
    • Improves the data abstraction syntax in Coco to allow a type to be abstracted only in some cases, rather than in all cases.
  • Improves @verify to correctly handle arrays of unverified types.
  • Improve outline view in Eclipse to show more symbols.
  • Fixed a bug that caused an Internal Error to be given during verification when using abort() as an expression.
  • Fixed a bug where @CPP.mapToType and @CPP.mapToValue were erroneously allowed on Coco-defined structs and enums.

1.0.0-beta.11 (18/09/2019)

  • Improves the single-threaded runtime to ensure that drainQueue() aligns correctly between provided ports and components. This also adds the drainQueue() event to counterexamples.
  • Improves the performance of the verification when verifying large multi-client models.
  • Allows _ to be used as the name of a parameter of a transition within a component state machine, thus allowing the parameter to be ignored, and no name to be generated for the parameter in the corresponding C++ code.
  • Adds a compatability mode for the generated C++ code with G++4.8.
  • Adds a function, purge() that purges all required ports of a component.
  • Improves consistency of how empty port state machines (i.e. ports with no functions) are handled.
  • Improves the formatter to always insert newlines for block-like type declarations.
  • Improves the generated C++ code to not have unused component_ variables.
  • Improves the generated C++ code to generate type aliases (using typedef or using, depending on the C++ standard being targeted) from Coco type aliases.
  • Fixes the display of signals sent to the chaotic client in multi-client counterexamples, which were previously marked as being sent to the normal user.
  • Fixed a crash when a verified parameter occured after a non-verified parameter.
  • Fixed a crash when displaying counterexamples that showed signals as being illegal.
  • Fixes an issue where some encapsulating components were incorrectly rejected due to connect statements overlapping.

1.0.0-beta.10 (10/09/2019)

  • Added the ability to generate header declarations for external functions where the CPP.mapToValue attribute is not applied.
  • Added an option, cocoRuntimeIncludeStyle, that allows the style of include used for the Coco runtime header to be specified.
  • Various improvements to the generated C++ code, including more use of inlines, removal of duplicate forward declarations, and full compatability with standards-compliant C++11.
  • Fixes a bug that resulted in Eclipse being unable to start following an upgrade.
  • Fixes CPP.mapToType when applied to type aliases.
  • Fixes coco_drain_queue being called on composite ports in the single-threaded runtime.
  • Fixes a crash when @coco.verify is applied only to the first parameter of a function.
  • Fixes a crash when showing eventually refinement counterexamples within Eclipse.
  • Fixes a crash when using equality patterns on tagged unions.

1.0.0-beta.9 (03/09/2019)

  • Added support for generating C++ code for: module-level constants, subscribe, unsubscribe, purge, setFilter, and unique.
  • Allow @coco.eventually to be used on ports in isolation to resolve port non-responsive errors.
  • Fixes an issue where @coco.verify was specified directly on port function parameters.

1.0.0-beta.8 (29/08/2019)

  • Allow @coco.noSideEffects to be applied to functions on ports, which requires all implementations of this function to have no side-effects.
  • Allows timer durations to be determined by calling a function on a required port.
  • Fixes generation of code within namespaces under C++.
  • Fixes occasional deadlocks when using the Eclipse plugin on Windows and Linux.
  • Fixes scrolling bugs in the counterexample viewer on Mac OS X.

1.0.0-beta.7 (22/08/2019)

  • Add support for automatically determining and authenticating to proxies on Windows.
  • Fixes spawning the license server on Windows.
  • Restore compatability of Linux release with RHEL-7.

1.0.0-beta.2 to 1.0.0-beta.6

  • Internal test releases.

1.0.0-beta.1 (02/08/2019)

  • First beta release of the Coco Platform for Eclipse.