add lower bound eval for file crdt

AntidoteDB · Jan 28, 2021 · 7d55b52 · 7d55b52
1 parent 284d47f
commit 7d55b52
Show file tree

Hide file tree

Showing 2 changed files with 67 additions and 3 deletions.
diff --git a/jvm/src/main/scala/crdtver/Repliss.scala b/jvm/src/main/scala/crdtver/Repliss.scala
@@ -487,9 +487,10 @@ object Repliss {
 
       val symbolicCheckThread: Future[LazyList[SymbolicExecutionRes]] = Future {
         if (checks contains SymbolicCheck()) {
-          symbolicCheckProgram(inputName, typedInputProg, runArgs)
+            LazyList()
+        //   symbolicCheckProgram(inputName, typedInputProg, runArgs)
             // only take checks until first procedure failing with exception
-            .takeUntil(_.exception.nonEmpty)
+            // .takeUntil(_.exception.nonEmpty)
         } else {
           LazyList()
         }

diff --git a/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala b/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala
@@ -25,6 +25,8 @@ class MVRegisterCrdt extends CrdtTypeDefinition {
 
   private val ReadPermsUpper = "ReadPermsUpper"
 
+  private val ReadPermsLower = "ReadPermsLower                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      "
+
   private val MvContains = "MvContains"
 
   override def additionalDataTypes: List[TypedAst.InTypeDecl] = List(
@@ -38,6 +40,7 @@ class MVRegisterCrdt extends CrdtTypeDefinition {
     dataType(MVRegisterQry, List("T"),List(
       dtCase(ReadFirst, List()),
       dtCase(ReadPermsUpper, List()),
+      dtCase(ReadPermsLower, List()),
       dtCase(MvContains, List("value" -> TypeVarUse("T")()))))
   )
 
@@ -53,7 +56,8 @@ class MVRegisterCrdt extends CrdtTypeDefinition {
 
     override def queryReturnType(q: QueryStructure): TypedAst.InTypeExpr = q match {
       case QueryStructure(ReadFirst, List()) => T
-      case QueryStructure(ReadPermsUpper, List()) => T
+      case QueryStructure(ReadPermsUpper, List()) => T                                                                                                                                                                                                                                                                                                              
+      case QueryStructure(ReadPermsLower, List()) => T
     }
 
     override def queryDefinitions(): List[TypedAst.InQueryDecl] = List(
@@ -125,6 +129,65 @@ class MVRegisterCrdt extends CrdtTypeDefinition {
             ))
         )
       }),
+      queryDeclEnsures(ReadPermsLower, List(), T, {
+        val result = varUse("result", T)
+        val result2 = varUse("result2", T)
+        val upperBound = varUse("result", T)
+        val someValue = varUse("someValue", T)
+        val someValue2 = varUse("someValue2", T)
+        val someAssign = varUse("someAssign", T)
+        val someAssign2 = varUse("someAssign", T)
+
+
+        val relevantCall = varUse("relevantCall")
+        val relevantCall2 = varUse("relevantCall2")
+        val otherCall = varUse("otherCall")
+        val otherCall2 = varUse("otherCall2")
+
+        // forall(relevantCall, forall(someAssign,
+        //     (   relevantCall.isVis
+        //         && relevantCall.op === makeOp(Assign, someAssign)
+        //         && not(exists(otherCall, exists(someValue, otherCall.isVis && relevantCall < otherCall && otherCall.op === makeOp(Assign, someValue))))
+        //         // all uninterrupted Assigns to the register
+        //     ) -->
+        //     (
+        //         (_upperBoundedByOrEq(someAssign, result)) && // upper bound
+        //         forall(upperBound,
+        //             (_upperBoundedBy(someAssign, upperBound)) -->
+        //             (_upperBoundedByOrEq(result, upperBound))
+        //         ) // lowest upper bound
+        //     )
+        // ))
+
+        forall(relevantCall, forall(someAssign,
+            (   relevantCall.isVis
+                && relevantCall.op === makeOp(Assign, someAssign)
+                && not(exists(otherCall, exists(someValue, otherCall.isVis && relevantCall < otherCall && otherCall.op === makeOp(Assign, someValue))))
+                // all uninterrupted Assigns to the register
+            ) -->
+            (
+                (_lowerBoundedByOrEq(someAssign, result))// upper bound 
+            )
+        )) &&
+        (
+        forall(result2,
+            (
+                forall(relevantCall2, forall(someAssign2,
+                (
+                    relevantCall2.isVis
+                    && relevantCall2.op === makeOp(Assign, someAssign2)
+                    && not(exists(otherCall2, exists(someValue2, otherCall2.isVis && relevantCall2 < otherCall2 && otherCall2.op === makeOp(Assign, someValue2))))
+                ) -->
+                (
+                    _lowerBoundedByOrEq(someAssign2, result2)
+                )
+                ))
+            ) -->
+            (
+                _lowerBoundedByOrEq(result, result2)
+            ))
+        )
+      }),
       {
         val x = "x" :: new TypeExtensions(T)
         queryDeclImpl(MvContains, List(x), T, {