Example: trying to run `apalache-mc check` on `CoffeeCan.tla`

Apalache Questions
1

This is an example question.

Hi,

I am running apalache-mc check CoffeeCan.tla on CoffeeCan.tla from the TLA+ examples. The model checker fails with the following message:

PASS #0: SanyParser
Parsing file [redacted]/tlaplus-examples/specifications/CoffeeCan/CoffeeCan.tla
Parsing file
[...]
PASS #1: TypeCheckerSnowcat
 > Running Snowcat .::.
CoffeeCan.tla:44:11-44:13: type input error: Expected a type annotation for VARIABLE can

What am I doing wrong? Any help is appreciated.

Cheers,
Igor

2

Hi Igor,

In contrast to TLC, Apalache infers types for the TLA+ specifications. However, it cannot infer all the types, especially the types of CONSTANTS and VARIABLES. To make your specification work with Apalache, you have to annotate the types of CONSTANTS and VARIABLES. The Typechecker tutorial explains how to write type annotations.

Looking at CoffeeCan.tla, it looks like the annotations should be like follows:

CONSTANT
  \* @type: Int;
  MaxBeanCount

VARIABLES
  \* @type: { black: Int, white: Int };
  can

Hope this helps!

Cheers,
Igor