Re: Error when adding an Invariant

[amit...@xxxxxxxxx]

Hi all, I have a spec which reproduces the problem on toolbox version 1.5.1 (June 2015). I'm running this on my Ubuntu 14.04 64bit and getting the following error:
Evaluating invariant 'No value in valueList [] for 0. Bug in TLCModelLaunchDataProvider.' failed.
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. TypeInvariant
1. Line 77, column 21 to line 77, column 88 in SysOverview


I'm a newbie so maybe I'm doing something wrong, but you can try to reproduce it with the following configuration:
Json <- {3,4}
Client <- {1,2}
ReqType <- {"Landscape", "Get", "Delete", "Create", "Update"}
Request(c,type,id,data) <- TRUE
Response(c,data) <- TRUE
and override Nat to be 1..3

Testing Spec works fine with no errors. Adding the TypeInvariant as an invariant to check results in the error.



---------------------------- MODULE SysOverview ----------------------------
EXTENDS Integers, Sequences

VARIABLE entity,      \* Ids of all the entities in the graph
         graph,       \* the graph, modeled as a function from entity ids to their Json representation
         ctrl,        \* control of all clients (one of ready, busy, done)
         buf          \* buffer containing requests to the graph and responses from the graph

CONSTANT Request(_,_,_,_),  \* An abstract "request to graph" step, hiding Neo4J HA cluster behavior
         Response(_,_),     \* An abstract "response from graph" step, hiding Neo4J HA cluster behavior
         Client,            \* Ids of all service instances which can talk to the graph on behalf of clients
         Json,              \* Values of entities
         ReqType            \* Possible types of requests
         
\* represent a non-value         
NoVal == CHOOSE v : v \notin (Json \cup Nat)

\* represent a dummy landscape for simplicity
landscape == CHOOSE v : v \notin (Json \cup Nat \cup {NoVal})

\* clients can request a "landscape" sub-graph around an entity, or perform CRUD operations
GraphReq == [type: {"Landscape"}, id: Nat, data: {NoVal}] 
            \cup [type: {"Get", "Delete"}, id: Nat, data: {NoVal}]
            \cup [type: {"Create", "Update"}, id: Nat, data: Json]


\* communication with the cluster can either succeed or fail
ASSUME \A c \in Nat, req \in ReqType, id \in Nat, data \in Json: 
                     /\ Request(c, req, id, data) \in BOOLEAN
                     /\ Response(c, data) \in BOOLEAN 


\* initially all clients are ready, graph and buffers are empty
Init == /\ entity = {}
        /\ graph = [e \in {} |-> Json]
        /\ ctrl = [c \in Client |-> "ready"]
        /\ buf = [c \in Client |-> NoVal]

\* request is enabled if the client is ready and the graph accepts the request                 
Req(c) == /\ ctrl[c] = "ready"
          /\ \E req \in GraphReq :
                 /\ Request(c,req.type, req.id, req.data)
                 /\ buf' = [buf EXCEPT ![c] = req]
                 /\ ctrl' = [ctrl EXCEPT ![c] = "busy"]
          /\ UNCHANGED <<entity, graph>>

\* perform the required changes on the graph when a request is pending and place the result in the buffer          
Do(c) == /\ ctrl[c] = "busy"
         /\ LET req == buf[c] IN
             /\ graph' = CASE req.type \in {"Create", "Update"} -> 
                                         [e \in (DOMAIN graph \cup {req.id}) |-> IF e = req.id THEN req.data ELSE graph[e]]
                         [] req.type = "Delete" -> [e \in (DOMAIN graph \ {req.id}) |-> graph[e]]
                         [] OTHER -> graph
             /\ entity' = CASE req.type = "Create" -> entity \cup {req.id}
                         [] req.type = "Delete" -> entity \ {req.id}
                         [] OTHER -> entity
             /\ buf' = CASE (/\ req.type = "Get" 
                             /\ req.id \in entity) -> [buf EXCEPT ![c] = graph[req.id]]
                         [] (/\ req.type = "Landscape" 
                             /\ req.id \in entity) -> [buf EXCEPT ![c] = landscape] 
                         [] OTHER -> [buf EXCEPT ![c] = NoVal]
         /\ ctrl' = [ctrl EXCEPT ![c] = "done"]

\* when execution is acknowledged by the graph the client is ready again         
Resp(c) == /\ ctrl[c] = "done"
           /\ Response(c, buf[c])
           /\ ctrl' = [ctrl EXCEPT ![c] = "ready"]
           /\ UNCHANGED <<entity, graph, buf>>
           
Next == \E c \in Client: Req(c) \/ Do(c) \/ Resp(c)
Spec == Init /\ [][Next]_<<entity, graph, ctrl, buf>>
        /\ WF_<<entity, graph, ctrl, buf>>(Next)

\* types should be correct in all states of all behaviors        
TypeInvariant == /\ (entity # {} => graph \in [entity -> Json])
                 /\ ctrl \in [Client -> {"ready", "busy", "done"}]
                 /\ buf \in [Client -> GraphReq \cup Json \cup {NoVal} \cup {landscape}] 
                 
=============================================================================