Hi Leslie, thank you very much for your suggestion, after watching the lectures I was able to make it works. Here is a simple example that I made to test the solution proposed by
Stephan, where I use many instances of consensus, each one to choose on one value:
---------------------------- MODULE SimpleNConsensus ----------------------------
EXTENDS FiniteSets, Naturals
CONSTANT Value, N
VARIABLE consensusInst
ASSUME N \in Nat /\ N > 0
Instances == 1..N
vars == <<consensusInst>>
TypeOK == consensusInst \in [Instances -> SUBSET Value]
C(i) == INSTANCE Consensus WITH chosen <- consensusInst[i]
Init == /\ consensusInst \in [Instances -> SUBSET Value]
/\ \A i \in Instances: C(i)!Init
Choose(v) == /\ consensusInst' \in [Instances -> SUBSET Value]
/\ \A i \in DOMAIN consensusInst: v \notin consensusInst[i]
/\ \E i \in Instances:
/\ C(i)!Next
/\ consensusInst' = [consensusInst EXCEPT ![i] = @ \cup {v}]
/\ \A j \in Instances \ {i} : UNCHANGED consensusInst[j]
Next == \E v \in Value: Choose(v)
Spec == Init /\ [][Next]_vars
-----------------------------------------------------------------------------
(***************************************************************************)
(* Safety: At most one value is chosen for all instances *)
(***************************************************************************)
Inv == /\ TypeOK
/\ \A i \in Instances: Cardinality(consensusInst[i]) \leq 1
THEOREM Invariance == Spec => []Inv
-----------------------------------------------------------------------------
(***************************************************************************)
(* Liveness: A non-trivial value is eventually chosen for all instances *)
(***************************************************************************)
NonTriviality == \A i \in Instances: <>(consensusInst[i] # {} /\ consensusInst[i] \subseteq Value)
LiveSpec == Spec /\ WF_vars(Next)
THEOREM LivenessTheorem == LiveSpec => NonTriviality
=============================================================================
\* Modification History
\* Last modified Sat Oct 06 15:34:11 CEST 2018 by rodrigo
\* Created Wed Oct 03 17:25:53 CEST 2018 by rodrigo
Em sábado, 6 de outubro de 2018 10:51:57 UTC+2, Leslie Lamport escreveu:
If your spec were correct, TLC would not be able to handle it because
of a long-standing bug: it doesn't correctly handle parametrized
instantiation. I suspect that this bug is not hard to fix, but there
have always been more pressing issues to handle. It would make a nice
project for someone who wants to help.
About the bug, is there some issue already open for that? Or do you know where in the code, someone interested in helping, could start looking?
And thank you for taking your time on this!
Best