Start working on spec

cosmos · Oct 31, 2022 · 3f3e546 · 3f3e546
1 parent 2c42f87
commit 3f3e546
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 0 deletions.
diff --git a/x/ccv/provider/keeper/keymap_api.cfg b/x/ccv/provider/keeper/keymap_api.cfg
@@ -0,0 +1,9 @@
+CONSTANTS
+    p0 = p0
+    p1 = p1
+    p2 = p2
+SYMMETRY PIDSymmetry
+INIT Init
+NEXT Next
+INVARIANT LeastCountInvariant
+
diff --git a/x/ccv/provider/keeper/keymap_api.tla b/x/ccv/provider/keeper/keymap_api.tla
@@ -0,0 +1,27 @@
+---- MODULE keymap_api ----
+
+EXTENDS  Integers, Naturals, FiniteSets, Sequences, TLC
+
+Validators == 0..2
+
+VARIABLES
+    consumerIndex,
+    consumerIndexMatured,
+    mappings,
+    valsets
+
+Init ==
+    /\ consumerVscid = 1,
+    /\ consumerVscidMatured = 0,
+    /\ mappings = [],
+    /\ valsets = []
+
+Next ==
+    \/ Map(providerKey, consumerKey)
+    \/ Increase(providerKey, consumerKey)
+    \/ Map(providerKey, consumerKey)
+
+
+Inv == 
+
+====