Apalache does not support operators as CONSTANTS

[BGR360]

Description

Apalache's parsing pass fails if the TLA+ module has an operator (e.g., Foo(_, _)) as a CONSTANT.

Impact

This prevents me from abstracting my specs in the way I would like. Take, for example, MemoryInterface.tla from Specifying Systems:

-------------------------- MODULE MemoryInterface ---------------------------
VARIABLE memInt
CONSTANTS  Send(_, _, _, _),
           Reply(_, _, _, _),
           InitMemInt, 
           Proc,  
           Adr,  
           Val
(* ... *)
=============================================================================

This is a generic specification that is agnostic to the way that Send(_, _, _, _) and Reply(_, _, _, _) work.

I want to do the same thing with the system I'm trying to specify:

My CacheCoherence module

-------------------------- MODULE CacheCoherence -------------------------------
(**
 * Defines the cache coherence property in a generic way.
 *)

EXTENDS Integers, Apalache

CONSTANTS
    \* The set of all process identifiers.
    \* @type: Set(PID);
    Pid,
    \* The set of all valid addresses.
    \* @type: Set(ADDR);
    Addr,
    \* The set of all values that can be stored in an address.
    \* @type: Set(VAL);
    Val,

    (**
     * Returns true iff the process is permitted to read from the provided
     * address in its cache in the current state.
     *
     * @type: (PID, ADDR) => Bool;
     *)
    ReadEnabled(_, _),

    (**
     * Returns true iff the process's cache contains the provided value at
     * the provided address in the current state.
     *
     * INVARIANT: If this 
     *
     * @type: (PID, ADDR, VAL) => Bool;
     *)
    Read(_, _, _)

(**
 * Data coherence invariant.
 *
 * If two processes' caches permit reads to the same address, then the data
 * in both caches is the same at that address.
 *)
Coherent ==
    \* For every pair of processes $p, q$, and every address $a$...
    \A p, q \in Pid, a \in Addr:
        \* If both processes enable reads to that address...
        (ReadEnabled(p, a) /\ ReadEnabled(q, a)) =>
            \* Then they contain the same value at address $a$.
            \E v \in Val: Read(p, a, v) /\ Read(q, a, v)

================================================================================

The only workaround I can think of is to introduce state variables that take the place of the operator parameters. I would really hate to have to do this, because then I'd have to waste state transitions updating the readEnabled variable rather than computing it from the other state variables.

I'm still pretty new to TLA+, so if anybody knows a different way to do what I want, please tell me!

Input specification

Here's an abbreviated repro:

---- MODULE ConstantOperator ----

CONSTANTS
    \* @type: Set(Int);
    A,
    \* @type: Set(Int);
    B,
    \* Whether two numbers are good together.
    \* @type: (Int, Int) => Bool;
    AreGood(_, _)

GOOD_PAIR_EXISTS == \E a \in A, b \in B: AreGood(a, b)

====

The command line parameters used to run the tool

$ apalache-mc --debug typecheck ConstantOperator.tla

Expected behavior

Typechecking succeeds.

Log files

Command line output:

# Tool home: /Users/ben/Documents/TLA+/apalache-0.30.1/bin
# Package:   /Users/ben/Documents/TLA+/apalache-0.30.1/bin/../lib/apalache.jar
# JVM args:  -Xmx4096m
#
22:39:27.597 [main] INFO at.forsyte.apalache.tla.tooling.opt.TypeCheckCmd - Loading configuration
# Usage statistics is OFF. We care about your privacy.
# If you want to help our project, consider enabling statistics with config --enable-stats=true.

Output directory: /Users/ben/Documents/TLA+/Bugs/_apalache-out/ConstantOperator.tla/2023-01-27T22-39-27_16203934688047097729
# APALACHE version: 0.30.1 | build: d447364                       I@22:39:27.818
Type checking ConstantOperator.tla                                I@22:39:27.826
PASS #0: SanyParser                                               I@22:39:27.942
Parsing file /Users/ben/Documents/TLA+/Bugs/ConstantOperator.tla
Parsing error: Unsupported operator type: line 10, col 5 to line 10, col 17 of module ConstantOperator E@22:39:28.063
Type checker [FAILED]                                             I@22:39:28.083
It took me 0 days  0 hours  0 min  0 sec                          I@22:39:28.083
Total time: 0.263 sec                                             I@22:39:28.083
EXITCODE: ERROR (255)

detailed.log:

2023-01-27T22:39:27,818 [main] INFO  a.f.a.t.Tool$ - # APALACHE version: 0.30.1 | build: d447364
2023-01-27T22:39:27,826 [main] INFO  a.f.a.t.t.o.TypeCheckCmd - Type checking ConstantOperator.tla
2023-01-27T22:39:27,942 [main] INFO  a.f.a.i.p.PassChainExecutor$ - PASS #0: SanyParser
2023-01-27T22:39:28,063 [main] ERROR a.f.a.t.p.i.SanyParserPassImpl - Parsing error: Unsupported operator type: line 10, col 5 to line 10, col 17 of module ConstantOperator
2023-01-27T22:39:28,083 [main] DEBUG a.f.a.i.p.PassChainExecutor$ - PASS #0: SanyParser [FAIL]
2023-01-27T22:39:28,083 [main] INFO  a.f.a.t.Tool$ - Type checker [FAILED]
2023-01-27T22:39:28,083 [main] INFO  a.f.a.t.Tool$ - It took me 0 days  0 hours  0 min  0 sec
2023-01-27T22:39:28,083 [main] INFO  a.f.a.t.Tool$ - Total time: 0.263 sec

System information

• Apalache version: 0.30.1
• OS: MacOS Monterey 12.3.1
• JDK version [e.g. OpenJDK 0.8.0]:

  java 17.0.2 2022-01-18 LTS
  Java(TM) SE Runtime Environment (build 17.0.2+8-LTS-86)
  Java HotSpot(TM) 64-Bit Server VM (build 17.0.2+8-LTS-86, mixed mode, sharing)
  

Additional context

I looked around the source code a little bit. Here's where the error is raised:

https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/OpApplTranslator.scala#L49-L68

It's possible that this is a bug in SANY and not in Apalache. I didn't get a good grasp of the way that Apalache does parsing in the little bit of time I spent reading.

If somebody gives me clear direction I'm happy to try fixing the bug myself.

Triage checklist (for maintainers)

• Reproduce the bug on the main development branch.
• Add the issue to the apalache GitHub project.
• If the bug is high impact, ensure someone available is assigned to fix it.

[BGR360]

Okay, I managed to hack together a fix to the problem (#2389). Let me know what you think :)