added the CIDSTORINGNODESAUDITLOG invariant.

vinahradau · Jul 4, 2020 · 817e66e · 817e66e
1 parent 8671cbd
commit 817e66e
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/CIDFINMA_spec_Z.zed16 b/CIDFINMA_spec_Z.zed16
@@ -90,8 +90,11 @@ Specification requirements:
 └
 ┌ CIDSTORINGNODESAUDITLOG
   cidStoringNodesIds: ℙ NODEID
+  NODE
 |
    #(cidStoringNodesIds) < 6
+   ∀ cidDataCategory : ran nodeDataCategories ⦁ 
+   cidDataCategory ∈ CIDCATEGORIES ⇒ nodeId ∈ cidStoringNodesIds
 └
 ┌ CIDBULKLOG
   cidBulkAccess: USER ↔ NODEID