[BUG] Fairness constraints cause bogus warning about Spec not in canonical form

[lemmy]

The example below has been fixed. For a follow up, see #468 (comment)

markus@avocado:~/Desktop/ewd998$ apalache check --config=EWD998.cfg EWD998.tla
# Tool home: /home/markus/src/TLA/_community/apalache
# Package:   /home/markus/src/TLA/_community/apalache/mod-distribution/target/apalache-pkg-0.8.2-SNAPSHOT-full.jar
# JVM args: -Xmx4096m -DTLA-Library=/home/markus/src/TLA/_community/apalache/src/tla
#
# APALACHE version 0.8.2-SNAPSHOT build v0.7.2-163-gde4505d
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/informalsystems/apalache/issues]
# 
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.

Checker options: filename=EWD998.tla, init=, next=, inv=          I@11:41:19.936
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.google.inject.internal.cglib.core.$ReflectUtils$1 (file:/home/markus/src/TLA/_community/apalache/mod-distribution/target/apalache-pkg-0.8.2-SNAPSHOT-full.jar) to method java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int,java.security.ProtectionDomain)
WARNING: Please consider reporting this to the maintainers of com.google.inject.internal.cglib.core.$ReflectUtils$1
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
PASS #0: SanyParser                                               I@11:41:20.958
Parsing file /home/markus/Desktop/ewd998/EWD998.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
PASS #1: ConfigurationPass                                        I@11:41:22.111
  > EWD998.cfg: Loading TLC configuration                         I@11:41:22.115
Operator Spec of 0 arguments is defined as: (Init() ∧ ☐([Next()]_vars())) ∧ (WF_vars()(System())) E@11:41:22.300
Configuration error (see the manual): EWD998.cfg: Expected Spec to be in the canonical form Init /\ [][Next]_vars /\ ... E@11:41:22.302
It took me 0 days  0 hours  0 min  2 sec                          I@11:41:22.304
Total time: 2.374 sec                                             I@11:41:22.304
EXITCODE: ERROR (99)

------------------------------- MODULE EWD998 -------------------------------
EXTENDS Integers, FiniteSets

CONSTANT N
ASSUME NAssumption == N \in Nat \ {0} \* At least one node.

Nodes == 0 .. N-1
Color == {"white", "black"}
Token == [pos : Nodes, q : Int, color : Color]

\* igor: this is the apalache idiom to deal with dynamic ranges
rng(a, b) == { i \in 0..N: a <= i /\ i <= b }

\* old apalache type annotations, will change soon
a <: b == a
\* a type specification for the recursive function reduced
reducedT == [Int -> Int]

MyReduce(op(_,_), fun, from, to, base) == 
  (**************************************************************************)
  (* Reduce the elements in the range from..to of the function's co-domain. *)
  (**************************************************************************)
  LET reduced[i \in rng(from, to)] ==
          IF i = from THEN op(base, fun[i])
          ELSE op((reduced <: reducedT)[i - 1], fun[i])
  IN reduced[to]

VARIABLES 
 active,     \* activation status of nodes
 color,      \* color of nodes
 counter,    \* nb of sent messages - nb of rcvd messages per node
 pending,    \* nb of messages in transit to node
 token       \* token structure
  
vars == <<active, color, counter, pending, token>>

TypeOK ==
  /\ active \in [Nodes -> BOOLEAN]
  /\ color \in [Nodes -> Color]
  /\ counter \in [Nodes -> Int]
  /\ pending \in [Nodes -> Nat]
  \* igor: instead of a membership over an infinite set, use Skolemization
  /\ \E p \in Nodes, q \in Int, c \in Color:
    token = [pos |-> p, q |-> q, color |-> c]
  \*/\ token \in Token
------------------------------------------------------------------------------
 
Init ==
  (* EWD840 but nodes *) 
  /\ active \in [Nodes -> BOOLEAN]
  /\ color \in [Nodes -> Color]
  (* Rule 0 *)
  /\ counter = [i \in Nodes |-> 0] \* c properly initialized
  /\ pending = [i \in Nodes |-> 0]
  /\ token = [pos |-> 0, q |-> 0, color |-> "black"]

InitiateProbe ==
  (* Rules 1 + 5 + 6 *)
  /\ token.pos = 0
  /\ \* previous round not conclusive if:
     \/ token.color = "black"
     \/ color[0] = "black"
     \/ counter[0] + token.q > 0
  /\ token' = [pos |-> N-1, q |-> 0, color |-> "white"]
  /\ color' = [ color EXCEPT ![0] = "white" ]
  \* The state of the nodes remains unchanged by token-related actions.
  /\ UNCHANGED <<active, counter, pending>>                            
  
PassToken(i) ==
  (* Rules 2 + 4 + 7 *)
  /\ ~ active[i] \* If machine i is active, keep the token.
  /\ token.pos = i
  /\ token' = [token EXCEPT !.pos = @ - 1,
                            !.q = @ + counter[i],
                            !.color = IF color[i] = "black" THEN "black" ELSE @]
  /\ color' = [ color EXCEPT ![i] = "white" ]
  \* The state of the nodes remains unchanged by token-related actions.
  /\ UNCHANGED <<active, counter, pending>>

System == \/ InitiateProbe
          \/ \E i \in Nodes \ {0} : PassToken(i)

-----------------------------------------------------------------------------

SendMsg(i) ==
  \* Only allowed to send msgs if node i is active.
  /\ active[i]
  (* Rule 0 *)
  /\ counter' = [counter EXCEPT ![i] = @ + 1]
  \* Non-deterministically choose a receiver node.
  /\ \E j \in Nodes \ {i} : pending' = [pending EXCEPT ![j] = @ + 1]
          \* Note that we don't blacken node i as in EWD840 if node i
          \* sends a message to node j with j > i
  /\ UNCHANGED <<active, color, token>>

RecvMsg(i) ==
  /\ pending[i] > 0
  /\ pending' = [pending EXCEPT ![i] = @ - 1]
  (* Rule 0 *)
  /\ counter' = [counter EXCEPT ![i] = @ - 1]
  (* Rule 3 *)
  /\ color' = [ color EXCEPT ![i] = "black" ]
  \* Receipt of a message activates i.
  /\ active' = [ active EXCEPT ![i] = TRUE ]
  /\ UNCHANGED <<token>>                           

Deactivate(i) ==
  /\ active[i]
  /\ active' = [active EXCEPT ![i] = FALSE]
  /\ UNCHANGED <<color, counter, pending, token>>

Environment == \E i \in Nodes : SendMsg(i) \/ RecvMsg(i) \/ Deactivate(i)

-----------------------------------------------------------------------------

Next ==
  System \/ Environment

Spec == Init /\ [][Next]_vars /\ WF_vars(System)  \* <== FAIRNESS
=======

SPECIFICATION Spec
CONSTANT N=3

[konnov]

Thanks! I will fix that.

[Alexander-N]

Another example of the same problem:

apalache check crdt.tla

gives me

PASS #1: ConfigurationPass                                        I@16:59:52.550
  > crdt.cfg: Loading TLC configuration                           I@16:59:52.554
Operator Spec of 0 arguments is defined as: (Init() ∧ ☐([Next()]_vars())) ∧ (WF_vars()(DeliverOnNode())) E@16:59:52.663
Configuration error (see the manual): crdt.cfg: Expected Spec to be in the canonical form Init /\ [][Next]_vars /\ ... E@16:59:52.666

crdt.tla

---- MODULE crdt ----
EXTENDS TLC, FiniteSets, Naturals, Sequences
CONSTANTS MAX_TIMESTAMP, KEYS, VALUES, N_NODES
VARIABLES timestamp, values, deliverQueues

vars == <<timestamp, values, deliverQueues>>
nodeIds == 1..N_NODES

DeliverSet(n, t, k, v) ==
  LET previous == { <<tp, kp, vp>> \in values[n]: kp = k }  IN
  IF previous = {} \/ \A <<tp, kp, vp>> \in previous : tp < t THEN
    values' = [ values EXCEPT ![n] = (values[n] \ previous) \union {<<t, k, v>>} ]
  ELSE
    UNCHANGED values

DeliverDelete(n, t) ==
  values' = [values EXCEPT ![n] = {<<tp, k, v>> \in values[n] : tp /= t }]

Deliver(n, command, payload) ==
  \/ command = "set"
    /\ DeliverSet(n, payload[1], payload[2], payload[3])
  \/ command = "delete"
    /\ DeliverDelete(n, payload)

Broadcast(n, command, payload) ==
  /\ Deliver(n, command, payload)
  /\ deliverQueues' = [
      i \in nodeIds |->
        IF i = n THEN
          deliverQueues[i]
        ELSE
          Append(deliverQueues[i], <<command, payload>>)
      ]

RequestSet(n, k, v) ==
  /\ timestamp' = timestamp + 1
  /\ Broadcast(n, "set", <<timestamp, k, v>>)

RequestDelete(n, k) ==
  \E <<t, kp, v>> \in values[n] :
    /\ kp = k
    /\ Broadcast(n, "delete", t)

RequestSetOnNode ==
  /\ timestamp < MAX_TIMESTAMP
  /\ \E <<n, k, v>> \in nodeIds \X KEYS \X VALUES : RequestSet(n, k, v)

RequestDeleteOnNode ==
  /\ \E <<n, k>> \in nodeIds \X KEYS : RequestDelete(n, k)
  /\ UNCHANGED timestamp

DeliverOnNode ==
  \E n \in nodeIds :
    /\ Len(deliverQueues[n]) > 0
    /\ \E <<command, payload>> \in {Head(deliverQueues[n])} :
        Deliver(n, command, payload)
    /\ deliverQueues' = [deliverQueues EXCEPT ![n] = Tail(deliverQueues[n])]
  /\ UNCHANGED timestamp

DeliverQueuesIsEmpty ==
  \A n \in nodeIds: Len(deliverQueues[n]) = 0

Terminating ==
  /\ DeliverQueuesIsEmpty
  /\ UNCHANGED vars

Init ==
  /\ values = [i \in nodeIds |-> {}]
  /\ deliverQueues = [i \in nodeIds |-> <<>>]
  /\ timestamp = 1

Next ==
  \/ RequestSetOnNode
  \/ RequestDeleteOnNode
  \/ DeliverOnNode
  \/ Terminating

Spec == Init /\ [][Next]_vars /\ WF_vars(DeliverOnNode)

AllValuesEqual ==
  \A <<n1, n2>> \in nodeIds \X nodeIds :
    values[n1] = values[n2]
EventuallyConsistent == <>[]AllValuesEqual
====

crdt.cfg

SPECIFICATION Spec

CONSTANTS
    MAX_TIMESTAMP = 3
    KEYS = {key}
    VALUES = {value}
    N_NODES = 2

PROPERTIES
    EventuallyConsistent

[konnov]

We are going to fix several bugs for the specs mentioned here and cut a new release on Monday

[konnov]

This is fixed now and will be included in the release (today). @lemmy, @Alexander-N, if you have further problems with your specs, open an issue or we could chat on zulip.

[lemmy]

The current fix is too narrow:

---- MODULE M ----
EXTENDS Integers

VARIABLE
    \* @type: Int;
    x

Init ==
    x = 0

Next ==
    x' \in 0..42

\* No problem if  F  is in-lined.
F ==
    WF_x(Next)

\* Fails with Configuration error (see the manual): M.cfg: Expected Spec to be in the canonical form Init /\ [][Next]_vars /\ ... E@10:51:44.946
SpecF1== Init /\ [][Next]_x /\ F   \* This is not uncommon
SpecF2 == x = 0 /\ [][Next]_x /\ WF_x(Next)
SpecF3 == Init /\ [][x' \in 0..42]_x /\ WF_x(Next)

\* Works
SpecW1 == Init /\ [][Next]_x /\ WF_x(Next)
SpecW2 == Init /\ [][Next]_x /\ WF_x(x' \in 0..42)  \* Compare SpecF3
====

APALACHE version 0.15.7-SNAPSHOT build v0.15.6-11-g95c1068

[lemmy]

Btw. it would be nice if --config=SomeConfigFile.cfg could be --config SomeConfigFile.cfg to make the shell's tab-completion work.

[konnov]

Yeah, you are right. We should fix the spec. As for the --config, we are using an option parser that works that way. Still looking for a good replacement :(

[fan-tom]

This specification

Spec == /\ Init /\ [][Next]_vars
        /\ \A self \in servers : WF_vars(server(self))

Produced by translaction of this PlusCal algorithm

-------------------------- MODULE mod --------------------------
CONSTANT
    \* @type: Int;
    defaultInitValue,
    \* @type: Set(SERVER);
    servers
VARIABLES
    \* @type: SERVER -> Str;
    pc,
    \* @type: Int;
    s

Inv == TRUE
(*--algorithm main
variables s;
fair process server \in servers
begin
    Start:
    s := 1;
end process;
end algorithm; *)
=====================================================================

Also gives the same error when checked with config mod.cfg

SPECIFICATION Spec
CONSTANT
defaultInitValue = 0
servers = { "s1_OF_SERVER", "s2_OF_SERVER" }
INVARIANT Inv

apalache-mc check --config=mod.cfg mod.tla