Hi colleagues, could you help me to figure out how to port attached TLA+ spec to Apalache?
I have a stack of structs but have hard time trying to specify Apalache type annotation for it.
I think problem is that I’m mixing functions, sequences and tuples which are all different for type checker. But I’m not sure how express stack using just one of them.
$ cat Test.tla
---- MODULE Test ----
EXTENDS
Integers, Sequences
CONSTANTS
\* @type: Int;
N
VARIABLES
\* @type: Seq({data : Int});
stack
\* How to make this a stack's type for Apalache ?
Stack == UNION {[1..len -> [data : 1..3]] : len \in 0..N}
Init ==
/\ stack = <<>>
Step ==
/\ Len(stack) = 0
/\ stack' = [stack EXCEPT ![Len(stack) + 1].data = 0]
Next ==
/\ Step
Spec ==
/\ Init
/\ [][Next]_<<stack>>
Inv ==
/\ stack \in Stack
/\ \A i \in DOMAIN stack : stack[i].data = 0
======================================================================
$ cat Init.cfg
CONSTANTS
N = 2
SPECIFICATION
Spec
INVARIANT
Inv
$ java -jar ./tla2tools.jar Test.tla
...
Model checking completed. No error has been found.
$ apalache-mc check --config=Test.cfg Test.tla
...
> Running Snowcat .::. I@16:12:53.664
[Test.tla:32:6-32:20]: An operator with the signature ((c, Set(c)) => Bool) cannot be applied to the provided arguments of type Seq({ data: Int }) and Set((Int -> { data: Int })) E@16:16:47.794