erreur de boîte à outils TLA + modèle en cours d'exécution: Valeur substituée Nat

Question

J'ai frappais l'erreur suivante dans la boîte à outils TLA + pendant quelques jours maintenant dans divers contextes:

"Attempted to compute the number of elements in the overridden value Nat.". 

Ce qui suit est le module le plus simple que je suis venu avec cela va reproduire le problème. J'ai vu quelques-unes des valeurs remplacées, mais je ne vois pas comment je fais quelque chose dans la spécification pour causer ce problème.

Quelqu'un voit-il l'erreur ou peut-il expliquer ce qui me manque?

-------------------------------- MODULE foo -------------------------------- 
EXTENDS Naturals 

VARIABLE Procs 

Init == Procs = 1..5 
Next == /\ Procs' = 1..5 

Entries == [ i \in Procs |-> [ j \in {} |-> 0] ] 
TypeOK == Entries \in [ Procs -> [ (SUBSET Nat) -> Nat ] ] 

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

Lors de la mise TypeOK à l'invariant, je reçois l'erreur complète

Attempted to compute the number of elements in the overridden value Nat. 
While working on the initial state: 
Procs = 1..5 

Answer 1

CCM ne peut pas évaluer l'ensemble Nat, parce qu'il est infini (voir aussi le overridden module Naturals.tla). Remplacer Nat avec un ensemble fini via le fichier de configuration est une solution de contournement possible.

Après cela, il se avère que TypeOK est FALSE, parce DOMAIN Entries = Procs et Procs # SUBSET Nat. En d'autres termes, l'ensemble [ (SUBSET Nat) -> Nat] contient des fonctions dont chacune a le domaine égal à SUBSET Nat. Au lieu de cela, ce qui était probablement prévu est l'ensemble des fonctions avec le domaine égal à certains sous-ensemble de Nat. Ceci est fait ci-dessous avec TypeOKChanged.

-------------------------------- MODULE foo -------------------------------- 
EXTENDS Naturals 

VARIABLE Procs 

Init == Procs = 1..5 
Next == Procs' = 1..5 

Entries == [ i \in Procs |-> [ j \in {} |-> 0] ] 
TypeOK == Entries \in [ Procs -> [ (SUBSET Nat) -> Nat ] ] 

TypeOKChanged == Entries \in [ Procs -> UNION {[Dom -> Nat]: Dom \in SUBSET Nat} ] 

NatMock == 0..6 
============================================================================= 

et le fichier de configuration foo.cfg:

INIT Init 
NEXT Next 

CONSTANTS Nat <- NatMock 
INVARIANT TypeOKChanged 

La sortie est

$ tlc2 foo.tla 
TLC2 Version 2.09 of 10 March 2017 
Running in Model-Checking mode with 1 worker. 
Parsing file foo.tla 
Parsing file ~/tlatools/tla/tla2sany/StandardModules/Naturals.tla 
Semantic processing of module Naturals 
Semantic processing of module foo 
Starting... (2017-10-15 16:00:06) 
Computing initial states... 
Finished computing initial states: 1 distinct state generated. 
Model checking completed. No error has been found. 
    Estimates of the probability that TLC did not check all reachable states 
    because two distinct states had the same fingerprint: 
    calculated (optimistic): val = 5.4E-20 
    based on the actual fingerprints: val = 1.1E-19 
2 states generated, 1 distinct states found, 0 states left on queue. 
The depth of the complete state graph search is 1. 
Finished in 03s at (2017-10-15 16:00:09) 

Une preuve impliquant l'ensemble infini Nat peut être poursuivi avec le théorème prouveur TLAPS. Voir aussi Sec. 14.2.3 aux pages 234-235 du TLA+ book la section "Don't Reinvent Mathematics".