Command-Line Tools¶

format¶

Automatically reformats all of the Coco files according to a specified style. In package mode, the settings specified in the [format] section will be used. In standalone mode, default formatting settings are used.

--verify¶

The specified files are not modified. Instead, the console output shows the changes that would be made to them to conform to the applicable format preference settings. In this case, the exit code of the tool will be 0 only when no changes need to be made, and will be 1 if the files are not correctly formatted.

Common generation options¶

--code-index-format <option>¶

Specify the format of the generated code index.

Option:	json Minimised JSON (i.e. no linebreaks, no spaces etc).
Option:	pretty-json Pretty-printed JSON.
Default:	json

--output-code-index <path>¶

If set to a path, then a code index of the generated code will be created.

See also

C++ Code Index for details on the C++ code index.

--output <path>, -o <path>¶

Specify the directory in which the generated C++ files are created. If the directory does not exist, it is automatically created. If it does exist, its contents are merged with any new files that are generated. If this option is not specified, then the default value is generated, relative to the current package.

--output-deps¶

Specify if gcc-style deps files with dependency information should be generated together with the generated files.

--output-empty-files¶

Coco will generate one header file and one implementation file for every Coco file processed, even if the file would be empty.

See also

generator.cpp.outputEmptyFiles

--output-unchanged-files¶

Normally the command-line tool will not update generated files whose contents have not changed. With this flag, the tool will touch files that have not changed if the timestamp of the .coco file from which they were generated is newer than the timestamp of the generated file. This flag is primarily for compatibility with timestamp-based build systems such as make.

See also

generator.cpp.outputUnchagedFiles

--restrict <path>¶

Only the specified header file or implementation file will be generated. Note that the given path must be the path of the file when it is output, and thus must start with the path given to --output.

generate-cpp¶

Generate C++ source files from the specified Coco files according to the preference settings in the [generator.cpp] section of applicable package file. In addition to the options below, the options from Common generation options are also permitted.

--header-file-suffix <string>¶

Equivalent to package.headerFileSuffix.

--header-for <path>¶

If path is a path to a .coco file, will cause the generator to only generate the header file corresponding to the given .coco file.

--include-prefix <path>¶

Prepend the specified path to all include paths in the generated code.

Option:	The path to prepend all include paths in the generated code.

--mocks <option>¶

Specify whether or not mocks should be generated and if so, which format should be used.

Option:	none No mocks are generated.
Option:	gmock Generate mocks compatible with the MOCK_METHOD macros.
Option:	gmock-legacy Generate mocks compatible with the old-style deprecated MOCK_METHODn macros.
Default:	none

--implementation-file-suffix <string>¶

Equivalent to package.implementationFileSuffix.

--implementation-for <path>¶

If path is a path to a .coco file, will cause the generator to only generate the implementation file corresponding to the given .coco file.

--output-runtime-header¶

Equivalent to package.outputRuntimeHeader.

graph-component¶

Produces a graphical representation of the architecture of a Coco component, like that produced in the Eclipse Architecture Diagram View. For example:

$ coco graph-component --component=Comp -o - src/M.coco

Will generate the architecture diagram of Comp in M.coco, and will write it to standard out.

--component <name>¶

The name of the component or port whose state machine should be graphed. This can be specified multiple times.

--hide-ports¶

Specifies that all ports should be hidden.

--multi¶

Specifies that multiple components can be graphed, which may result in multiple output files being produced.

--output <path>¶

The path to where to save the generated diagram. If this is not specified, then the file is placed alongside the .coco file. If this is set to ‘-‘, then the diagram is written to standard out.

graph-states¶

Produces a graphical representation of a state machine, like that produced in the Eclipse State Diagram View. For example:

$ coco graph-states --target=Comp -o - src/M.coco

This will generate the state diagram for the state machine of Comp in M.coco, and will write it to standard out.

--target <name>¶

The name of the component or port whose state machine should be graphed.

--format <option>¶

Option:	dot The Graphviz’s dot format will be used.
Option:	svg A SVG image will be produced.
Default:	svg

--hide-labels¶

Specify that all labels on transitions should be hidden in the generated diagram.

--output <path>¶

The path to where to save the generated diagram. If this is not specified, then the file is placed alongside the .coco file. If this is set to ‘-‘, then the diagram is written to standard out.

--separate-edges¶

Whether to produce a separate edge for each transition. By default transition edges are collapsed by generating one shared edge for all transitions between a given pair of states.

metadata¶

Outputs metdata about a Coco package, depending on the option that is selected:

--selected-tool-version¶

Prints the value of the tool.selectedVersion property to stdout, including interpreting any special values that are permitted as part of this property.

support-bundle¶

This command copies a project, together with all of its dependencies, and creates a single zip file that is suitable for sending to support@cocotec.io. This command is intended for sharing confidential projects with Cocotec, as in addition to bundling all the files together, the bundler also renames all Coco identifies to randomly chosen names in a semantically-preserving fashion, and removes all comments.

--output <path>¶

The path where the .zip file should be saved.

transform¶

Executes one of Coco’s semantically aware transformations. When operating in package mode, all files in the current package are transformed (depending on the transformation selected), whereas when operating in standalone mode, just the specified files are transformed.

The following options are common to all transformations:

--format <option>¶

Option:	none No files are formatted.
Option:	modified-files All modified files are formatted.
Default:	none

Specifies whether the transformed files should be automatically formatted using the Coco formatter.

--output-mode <option>¶

Option:	in-place Files are overwritten with the modified contents.
Option:	preview Modified files are printed to stdout.
Default:	in-place

Specifies where the results of the transformation should be saved.

--selection <name>¶

A fully qualified name to the declaration to apply the transformation to, or the string :all to specify that the transformation should be applied to all declarations that it makes sense to apply it to.

port Composite {
  port P1 {
    function f1() : Nil
  }
  port P2 {
    enum AnEnum {
      case AMember
      case AnotherMember
    }
    outgoing signal cb(y : AnEnum)
  }
  val p1 : P1
  val p2 : P2
  machine {
    state Operational {
      p.f1() = p2.cb(P2.AnEnum.AMember)
    }
  }
}

port Composite {
  function f1() : Nil
  enum AnEnum {
    case AMember
    case AnotherMember
  }
  outgoing signal cb(y : AnEnum)
  machine {
    state Operational {
      f1() = cb(AnEnum.AMember)
    }
  }
}

port P {
  function fn() : Nil
  outgoing signal fn_cb_OK()
  outgoing signal fn_cb_ERROR()
  machine M {
    fn() = nondet { fn_cb_OK(), fn_cb_ERROR() }
  }
}

port P {
  function fn() : Nil
  outgoing signal fn_cb(result : Result<Nil, Nil>)

  machine M {
    fn() = nondet { fn_cb(.Ok(nil)), fn_cb(.Error(nil)) }
  }
}

port Composite {
  enum E {
    case X
    case Y
  }

  function fn(x : Bool) : E

  machine M {
    fn(_ : Bool) = Composite.E.X
  }
}

enum E {
  case X
  case Y
}

external function fn(x : Bool) : E = E.X

typecheck¶

Checks that the specified Coco files are all type-correct. When operating in package mode, all files in the current package are typechecked, whereas when operating in standalone mode, just the specified files are typechecked.

verify¶

Verifies all of the specified Coco files. When operating in package mode, all files in the current package are verified, whereas when operating in standalone mode, just the specified files are verified.

--backend <option>¶

Specify which verification backend is to be used.

Option:	local Verification is performed locally.
Option:	attempt-remote If the remote verification service is available, verification is carried out using the remote service. Otherwise, it is carried out locally.
Option:	remote Verification is carried out using the remote verification service only, raising an error if it is not reachable.
Default:	if a preference has been set in Eclipse, then that is used, otherwise local.

--benchmark¶

Output performance data that can be used for verification benchmark comparisons.

--ignore-cache¶

Ignores all cached verification results when using the remote verification backend.

--format <option>¶

Specify verification output format.

Option:	junit Verification output is formatted as JUnit-compatible XML.
Option:	console Verification output is formatted as text.
Default:	console

--quiet¶

Suppresses progress information that is normlaly output whilst the verification is running.

--max-local-jobs¶

The maximum number of verification jobs that should be executed concurrently when running verification on the local machine.

Licensing¶

To use Coco as part of a continuous integration (CI) pipeline, each machine that coco executes on will require a license. Since CI machines are often ephemeral, it can be inconvienient to license them using the usual interactive commands. Instead, Coco can be configured to use a license token that is not tied to any specific machine, but can instead be exchanged by a specific machine for a real license when it is required by connecting to a license server. Further, this license server can either be run on-premise, or Cocotec’s licensing server can be used, providing the CI machines are able to access the internet.

To setup Coco to use a machine token:

1. Contact support@cocotec.io to request a machine license token, unless your organisation already has an existing on-premise license server in which case please contact your local administrators. When contacting Cocotec Support, please indicate if you require a on-premise license server to be setup, or if your CI systems have access to the internet and can therefore use Cocotec’s licensing servers.

2. Store the machine license token securely using whatever secret storage mechanism you use. For example, common CI providers have builtin solutions for storing secrets:

   • Jenkins
   • Github Actions

3. Configure your CI pipeline to pass the authentication token to coco. The best way of doing this depends upon the number of times that you execute coco during the build:

   • coco is only executed once:

     Set the environment variable COCOTEC_AUTH_TOKEN to the value of machine token before executing coco. coco will read this environment variable and then connect to the appropriate license server to obtain a license.

   • coco is executed multiple times:

     To avoid the overhead of connecting to the license server everytime coco is invoked, it is instead best to obtain a license up-front, and then reuse the license for the rest of the pipeline. This can be done by firstly executing cocotec-licensing-server to obtain the license, and then passing the cached license to coco. For example:

     $ export COCO_LICENSE_CACHE_FILE=<path>
     $ cocotec-licensing-server --acquire=coco-platform --license-file=$COCO_LICENSE_CACHE_FILE
     ...
     $ coco --no-license-server --override-licenses=$COCO_LICENSE_CACHE_FILE
     

     This will obtain a license using cocotec-licensing-server and then save the path specified in $COCO_LICENSE_CACHE_FILE. When coco is executed later, it will use the license that was obtained earlier. To make this work, cocotec-licensing-server has to be supplied the machine authentication token. This can be done either by setting the COCOTEC_AUTH_TOKEN environment variable only when invoking cocotec-licensing-server:

     COCOTEC_AUTH_TOKEN=... cocotec-licensing-server --acquire=coco-platform --license-file=$COCO_LICENSE_CACHE_FILE
     

     or, if the authentication token is available in a file called cocotec_token:

     cocotec-licensing-server --acquire=coco-platform --license-file=$COCO_LICENSE_CACHE_FILE --auth-token=cocotec_token