Added CIDSTORINGNODESAUDITLOG invariant.

vinahradau · Jul 4, 2020 · 3463d68 · 3463d68
1 parent 817e66e
commit 3463d68
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/CIDFINMA_spec_Z.zed b/CIDFINMA_spec_Z.zed
@@ -113,9 +113,11 @@ Specification requirements:
 
 
 \begin{schema}{CIDSTORINGNODESAUDITLOG}
- cidStoringNodesIds : \power NODEID 
+ cidStoringNodesIds : \power NODEID \\
+ NODE
 \where
- \# ( cidStoringNodesIds ) < 6
+ \# ( cidStoringNodesIds ) < 6\\
+ \forall cidDataCategory : \ran nodeDataCategories @ cidDataCategory \in CIDCATEGORIES \implies nodeId \in cidStoringNodesIds
 \end{schema}