From 6c8ff3920b3ada59283caf9c7b8fb061028f05d3 Mon Sep 17 00:00:00 2001 From: Michael Youssef Date: Mon, 25 Jan 2021 13:30:24 +0100 Subject: [PATCH 01/10] add crdt access rights --- .gitignore | 4 + .../scala/crdtver/language/InputAst.scala | 3 + .../crdtver/language/TypedAstHelper.scala | 9 ++ .../crdtver/language/TypedAstPrinter.scala | 2 + .../main/scala/crdtver/language/Typer.scala | 1 + .../language/crdts/FileAccessCrdt.scala | 148 ++++++++++++++++++ .../language/crdts/MVRegisterCrdt.scala | 29 ++++ .../crdtver/symbolic/ExprTranslation.scala | 11 ++ .../scala/crdtver/testing/Interpreter.scala | 2 + .../testing/LogicEvalTranslation.scala | 3 + 10 files changed, 212 insertions(+) create mode 100644 jvm/src/main/scala/crdtver/language/crdts/FileAccessCrdt.scala diff --git a/.gitignore b/.gitignore index 9ab7a18..ee5fd8c 100644 --- a/.gitignore +++ b/.gitignore @@ -10,3 +10,7 @@ act/ jvm/src/main/resources/native jvm/src/main/resources/scalajs jvm/src/main/resources/versioninfo.properties +.vscode/ +.metals/ +project/ +.bloop/ \ No newline at end of file diff --git a/jvm/src/main/scala/crdtver/language/InputAst.scala b/jvm/src/main/scala/crdtver/language/InputAst.scala index bda3d93..5c29a37 100644 --- a/jvm/src/main/scala/crdtver/language/InputAst.scala +++ b/jvm/src/main/scala/crdtver/language/InputAst.scala @@ -276,6 +276,7 @@ object InputAst { function match { case BF_isVisible() => s"${args.head} is visible" case BF_happensBefore(_) => s"(${args.head} happens before ${args(1)})" + case BF_upperBoundedBy() => s"(${args.head} upper bounded by ${args(1)})" case BF_sameTransaction() => s"sameTransaction(${args(0)}, ${args(1)})" case BF_less() => s"(${args.head} < ${args(1)})" case BF_lessEq() => s"(${args.head} <= ${args(1)})" @@ -341,6 +342,8 @@ object InputAst { case class BF_happensBefore(on: HappensBeforeOn) extends BuiltInFunc() + case class BF_upperBoundedBy() extends BuiltInFunc() + sealed trait HappensBeforeOn object HappensBeforeOn { diff --git a/jvm/src/main/scala/crdtver/language/TypedAstHelper.scala b/jvm/src/main/scala/crdtver/language/TypedAstHelper.scala index d6765ff..fbfb539 100644 --- a/jvm/src/main/scala/crdtver/language/TypedAstHelper.scala +++ b/jvm/src/main/scala/crdtver/language/TypedAstHelper.scala @@ -93,6 +93,15 @@ object TypedAstHelper { ) } + def upperBoundedBy(exp1: InExpr, exp2: InExpr): ApplyBuiltin = { + ApplyBuiltin( + source = NoSource(), + typ = BoolType(), + function = BF_upperBoundedBy(), + args = List(exp1, exp2) + ) + } + def and(exp1: InExpr, exp2: InExpr): InExpr = (exp1, exp2) match { case (BoolConst(_, _, true), x) => x case (x@BoolConst(_, _, false), _) => x diff --git a/jvm/src/main/scala/crdtver/language/TypedAstPrinter.scala b/jvm/src/main/scala/crdtver/language/TypedAstPrinter.scala index ec248dc..dec7862 100644 --- a/jvm/src/main/scala/crdtver/language/TypedAstPrinter.scala +++ b/jvm/src/main/scala/crdtver/language/TypedAstPrinter.scala @@ -88,6 +88,8 @@ object TypedAstPrinter { function match { case BuiltInFunc.BF_isVisible() => printExpr(args(0)) <> ".isVisible" + case BuiltInFunc.BF_upperBoundedBy() => + printOp(args(0), "upperBound", args(1)) case BuiltInFunc.BF_happensBefore(on) => printOp(args(0), "happensBefore", args(1)) case BuiltInFunc.BF_sameTransaction() => diff --git a/jvm/src/main/scala/crdtver/language/Typer.scala b/jvm/src/main/scala/crdtver/language/Typer.scala index fbef687..acf1863 100644 --- a/jvm/src/main/scala/crdtver/language/Typer.scala +++ b/jvm/src/main/scala/crdtver/language/Typer.scala @@ -964,6 +964,7 @@ class Typer { val t = TypeVarUse("T")() bf match { case BF_isVisible() => p(List(CallIdType()) -> BoolType()) + case BF_upperBoundedBy() => PrincipleType(List(t), List(t, t) -> BoolType()) // TODOO: check case BF_happensBefore(_) => List( p(List(CallIdType(), CallIdType()) -> BoolType()), p(List(InvocationIdType(), InvocationIdType()) -> BoolType()) diff --git a/jvm/src/main/scala/crdtver/language/crdts/FileAccessCrdt.scala b/jvm/src/main/scala/crdtver/language/crdts/FileAccessCrdt.scala new file mode 100644 index 0000000..68bd2b8 --- /dev/null +++ b/jvm/src/main/scala/crdtver/language/crdts/FileAccessCrdt.scala @@ -0,0 +1,148 @@ +// package crdtver.language.crdts + +// import crdtver.language.TypedAst +// import crdtver.language.TypedAst.{BoolType, TypeVarUse} +// import crdtver.language.TypedAstHelper._ +// import crdtver.language.crdts.ACrdtInstance.{QueryStructure, printTypes} +// import crdtver.language.crdts.FlagCrdt.Strategy + +// class FileAccessCrdt extends CrdtTypeDefinition { + +// /** number of normal type parameters */ +// override def numberTypes: Int = 2 + +// /** number of CRDT type parameters */ +// override def numberInstances: Int = 0 + +// private val FAOp = "FAOp" + +// private val Assign = "Assign" + +// private val FAQry = "FAQry" + +// private val ReadFA = "ReadFA" + +// // predefined values for access rights +// private val None : TypedAst.InExpr = "None" // here is the problem, i cant define a InExpr type with single value for comparison in Strutegy + +// private val R : TypedAst.InExpr = "R" // here is the problem + +// private val W = "W" + +// private val X = "X" + +// private val RW = "RW" + +// private val RX = "RX" + +// private val WX = "WX" + +// private val RWX = "RWX" + +// // predefined values for user types + +// private val Admin = "Admin" + +// private val User = "User" + + +// override def additionalDataTypes: List[TypedAst.InTypeDecl] = List( +// dataType( +// FAOp, +// List("U", "V"), +// List( +// dtCase(Assign, List("user" -> TypeVarUse("U")(), "value" -> TypeVarUse("V")())) +// ) +// ), +// dataType(FAQry, List("V"), List(dtCase(ReadFA, List()))) +// ) + +// override def instantiate(typeArgs: List[TypedAst.InTypeExpr], crdtArgs: List[ACrdtInstance]): ACrdtInstance = new ACrdtInstance { +// val U: TypedAst.InTypeExpr = typeArgs.head // it should be User +// val V: TypedAst.InTypeExpr = (typeArgs.tail).head // make sure it will give the second item in list which must be Value + +// override def toString: String = s"${FileAccessCrdt.this.name}${printTypes(typeArgs, crdtArgs)}" + +// override def operationType: TypedAst.InTypeExpr = TypedAst.SimpleType(FAOp, List(U, V))() + +// override def queryType: TypedAst.InTypeExpr = TypedAst.SimpleType(FAQry, List(U, V))() + +// override def queryReturnType(q: QueryStructure): TypedAst.InTypeExpr = q match { +// case QueryStructure(ReadFA, List()) => V +// } + +// override def queryDefinitions(): List[TypedAst.InQueryDecl] = List( +// queryDeclEnsures(ReadFA, List(), V, { +// val result = varUse("result", V) +// val user1 = varUse("user1", U) +// val c = varUse("c") +// val c2 = varUse("c2") +// val v = varUse("v", V) +// val user2 = varUse("user2", U) +// not(exists(v, v !== None || v !== R || v !== W || v !== X || v !== RW || v !== RX || v !== WX || v !== RWX )) +// && +// not(exists(result, result !== None || result !== R || result !== W || result !== X || result !== RW || result !== RX || result !== WX || result !== RWX )) +// && +// not(exists(user1, user1 !== Admin || user1 !== User)) +// && +// not(exists(user2, user2 !== Admin || user2 !== User)) +// && + +// ( +// not(exists(c, exists(v, c.isVis && c.op === makeOp(Assign, user2, v) && user2 === Admin))) || +// ( +// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === R +// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && v === None +// ))) +// ) +// && +// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === W +// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && v === None //(v === None || v === R) +// ))) +// ) +// && +// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === E +// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && v === None //(v === None || v === R) +// ))) +// ) +// && +// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === RW +// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && (v === None || v === R || v === W ) +// ))) +// ) +// && +// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === RX +// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && (v === None || v === X || v === R ) +// ))) +// ) +// && +// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === WX +// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && (v === None || v === X || v === W ) +// ))) +// ) +// && +// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === RWX +// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && (v === None || v === R || v === W || X) +// ))) +// ) +// ) +// ) + +// && +// ( +// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === User +// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin +// ))) +// ) +// ) + +// }) + +// ) + +// override def additionalDataTypesRec: List[TypedAst.InTypeDecl] = FileAccessCrdt.this.additionalDataTypes +// } + +// /** name of the CRDT */ +// override def name: String = "FileAccessTuple" +// } diff --git a/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala b/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala index 2613603..6fc03e4 100644 --- a/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala +++ b/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala @@ -21,6 +21,8 @@ class MVRegisterCrdt extends CrdtTypeDefinition { private val ReadFirst = "ReadFirst" + private val ReadPermsUpper = "ReadPermsUpper" + private val MvContains = "MvContains" override def additionalDataTypes: List[TypedAst.InTypeDecl] = List( @@ -33,6 +35,7 @@ class MVRegisterCrdt extends CrdtTypeDefinition { ), dataType(MVRegisterQry, List("T"),List( dtCase(ReadFirst, List()), + dtCase(ReadPermsUpper, List()), dtCase(MvContains, List("value" -> TypeVarUse("T")())))) ) @@ -48,6 +51,7 @@ class MVRegisterCrdt extends CrdtTypeDefinition { override def queryReturnType(q: QueryStructure): TypedAst.InTypeExpr = q match { case QueryStructure(ReadFirst, List()) => T + case QueryStructure(ReadPermsUpper, List()) => T } override def queryDefinitions(): List[TypedAst.InQueryDecl] = List( @@ -60,6 +64,31 @@ class MVRegisterCrdt extends CrdtTypeDefinition { exists(c, c.isVis && c.op === makeOp(Assign, result) && not(exists(c2, exists(v, c2.isVis && c < c2 && c2.op === makeOp(Assign, v))))) }), + queryDeclEnsures(ReadPermsUpper, List(), T, { + val result = varUse("result", T) + val upperBound = varUse("result", T) + val someValue = varUse("someValue", T) + val someAssign = varUse("someAssign", T) + + + val relevantCall = varUse("relevantCall") + val otherCall = varUse("otherCall") + + 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 + ) --> + ( + (upperBoundedBy(someAssign, result) || someAssign === result) && // upper bound + forall(upperBound, + (upperBoundedBy(someAssign, upperBound)) --> + (upperBoundedBy(result, upperBound) || result === upperBound) + ) // lowest upper bound + ) + )) + }), { val x = "x" :: new TypeExtensions(T) queryDeclImpl(MvContains, List(x), T, { diff --git a/jvm/src/main/scala/crdtver/symbolic/ExprTranslation.scala b/jvm/src/main/scala/crdtver/symbolic/ExprTranslation.scala index cfd41aa..3b0d40f 100644 --- a/jvm/src/main/scala/crdtver/symbolic/ExprTranslation.scala +++ b/jvm/src/main/scala/crdtver/symbolic/ExprTranslation.scala @@ -59,6 +59,17 @@ object ExprTranslation { def translateBuiltin(expr: ApplyBuiltin)(implicit ctxt: SymbolicContext, state: SymbolicState): SVal[_ <: SymbolicSort] = { val args: List[SVal[_]] = expr.args.map(translateUntyped) expr.function match { + case BF_upperBoundedBy() => // TODOO: hard code + val left: SVal[SymbolicSort] = castSymbolicSort(args(0)) + val right: SVal[SymbolicSort] = castSymbolicSort(args(1)) + // automatically adapt to option types + // TODO maybe adapt to option types in the frontend + if (left.typ == SortOption(right.typ)) + SEq(castSymbolicSort(left), castSymbolicSort(SSome(right))) + else if (SortOption(left.typ) == right.typ) + SEq(castSymbolicSort(SSome(left)), castSymbolicSort(right)) + else + SEq(left, right) case BF_isVisible() => state.visibleCalls.contains(cast(args(0))) case BF_happensBefore(on) => diff --git a/jvm/src/main/scala/crdtver/testing/Interpreter.scala b/jvm/src/main/scala/crdtver/testing/Interpreter.scala index 782c20d..2818b10 100644 --- a/jvm/src/main/scala/crdtver/testing/Interpreter.scala +++ b/jvm/src/main/scala/crdtver/testing/Interpreter.scala @@ -529,6 +529,8 @@ case class Interpreter(val prog: InProgram, runArgs: RunArgs, val domainSize: In evalExpr(args(i), localState, state)(anyValueCreator) }) function match { + case BF_upperBoundedBy() => // TODOO: hardcode + anyValueCreator(true) case BF_isVisible() => anyValueCreator(localState.visibleCalls.contains(eArgs(0).value.asInstanceOf[CallId])) case BF_happensBefore(on) => diff --git a/jvm/src/main/scala/crdtver/testing/LogicEvalTranslation.scala b/jvm/src/main/scala/crdtver/testing/LogicEvalTranslation.scala index 67d432a..2612473 100644 --- a/jvm/src/main/scala/crdtver/testing/LogicEvalTranslation.scala +++ b/jvm/src/main/scala/crdtver/testing/LogicEvalTranslation.scala @@ -235,6 +235,9 @@ object LogicEvalTranslation { function match { case BuiltInFunc.BF_isVisible() => IsElem(argsT(0), env((e: InterpreterEnv) => e.localState.visibleCalls)) + case BuiltInFunc.BF_upperBoundedBy() => // TODOO: hard code + Eq(argsT(0), argsT(1)) + // op[(Expr[Any], Expr[Any]), Boolean](e => true, Pair(argsT(0), argsT(1))) case BuiltInFunc.BF_happensBefore(on) => on match { case HappensBeforeOn.Unknown() => unexpected(on) From be311c8e145d36f373eca3e2a5f547c284428256 Mon Sep 17 00:00:00 2001 From: Hussein Date: Tue, 26 Jan 2021 16:43:31 +0100 Subject: [PATCH 02/10] Midifying MultiValueRegister to provide qeury for AccessRight upper bound --- .../language/crdts/MVRegisterCrdt.scala | 111 ++++++++++++++++-- 1 file changed, 101 insertions(+), 10 deletions(-) diff --git a/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala b/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala index 6fc03e4..036fa92 100644 --- a/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala +++ b/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala @@ -4,6 +4,8 @@ import crdtver.language.{TypedAst, crdts} import crdtver.language.TypedAst.TypeVarUse import crdtver.language.TypedAstHelper._ import crdtver.language.crdts.ACrdtInstance.{QueryStructure, printTypes} +import crdtver.language.TypedAst.InExpr + class MVRegisterCrdt extends CrdtTypeDefinition { @@ -66,27 +68,58 @@ class MVRegisterCrdt extends CrdtTypeDefinition { }), queryDeclEnsures(ReadPermsUpper, 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 - ) --> + ( 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 ( - (upperBoundedBy(someAssign, result) || someAssign === result) && // upper bound - forall(upperBound, - (upperBoundedBy(someAssign, upperBound)) --> - (upperBoundedBy(result, upperBound) || result === upperBound) - ) // lowest 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)))) + ) --> + ( + _upperBoundedByOrEq(someValue2, result2) + ) + ))) --> + ( + _upperBoundedBy(result, result2) + ) ) + ) )) }), { @@ -102,6 +135,64 @@ class MVRegisterCrdt extends CrdtTypeDefinition { ) override def additionalDataTypesRec: List[TypedAst.InTypeDecl] = MVRegisterCrdt.this.additionalDataTypes + + def _upperBoundedBy(val1: InExpr, val2: InExpr): InExpr = ( + ( + val1 === makeOperation("R") && + (val2 === makeOperation("RW") || val2 === makeOperation("RX") || val2 === makeOperation("RWX")) + ) || + ( + val1 === makeOperation("W") && + (val2 === makeOperation("RW") || val2 === makeOperation("WX") || val2 === makeOperation("RWX")) + ) || + ( + val1 === makeOperation("X") && + (val2 === makeOperation("RX") || val2 === makeOperation("WX") || val2 === makeOperation("RWX")) + ) || + ( + val1 === makeOperation("RW") && + (val2 === makeOperation("RWX")) + ) || + ( + val1 === makeOperation("RX") && + (val2 === makeOperation("RWX")) + ) || + ( + val1 === makeOperation("WX") && + (val2 === makeOperation("RWX")) + ) + ) + + def _upperBoundedByOrEq(val1: InExpr, val2: InExpr): InExpr = ( + ( + val1 === makeOperation("R") && + (val2 === makeOperation("R") || val2 === makeOperation("RW") || val2 === makeOperation("RX") || val2 === makeOperation("RWX")) + ) || + ( + val1 === makeOperation("W") && + (val2 === makeOperation("W") || val2 === makeOperation("RW") || val2 === makeOperation("WX") || val2 === makeOperation("RWX")) + ) || + ( + val1 === makeOperation("X") && + (val2 === makeOperation("X") || val2 === makeOperation("RX") || val2 === makeOperation("WX") || val2 === makeOperation("RWX")) + ) || + ( + val1 === makeOperation("RW") && + (val2 === makeOperation("RW") || val2 === makeOperation("RWX")) + ) || + ( + val1 === makeOperation("RX") && + (val2 === makeOperation("RX") || val2 === makeOperation("RWX")) + ) || + ( + val1 === makeOperation("WX") && + (val2 === makeOperation("WX") || val2 === makeOperation("RWX")) + ) || + ( + val1 === makeOperation("RWX") && + val2 === makeOperation("RWX") + ) + ) } /** name of the CRDT */ From 495121548de2e46b10f59db839d331175b918b74 Mon Sep 17 00:00:00 2001 From: Peter Zeller Date: Tue, 26 Jan 2021 23:35:20 +0100 Subject: [PATCH 03/10] first steps towards random datatype value generation --- .../scala/crdtver/testing/Interpreter.scala | 13 ++++---- .../scala/crdtver/testing/RandomTester.scala | 30 ++++++++++++++++--- 2 files changed, 33 insertions(+), 10 deletions(-) diff --git a/jvm/src/main/scala/crdtver/testing/Interpreter.scala b/jvm/src/main/scala/crdtver/testing/Interpreter.scala index 2818b10..49d8989 100644 --- a/jvm/src/main/scala/crdtver/testing/Interpreter.scala +++ b/jvm/src/main/scala/crdtver/testing/Interpreter.scala @@ -858,15 +858,12 @@ case class Interpreter(val prog: InProgram, runArgs: RunArgs, val domainSize: In case None => customTypeDomain(name) case Some(dt1) => - // TODO substitute typeArgs val dt = dt1.instantiate(typeArgs) for (dtcase <- dt.dataTypeCases.to(LazyList); params <- enumerate(dtcase.params, state)) yield { val args = dtcase.params.map(p => params(LocalVar(p.name.name))) AnyValue(DataTypeValue(dtcase.name.name, args)) } } - // TODO handle datatypes - case idt@IdType(name) => state.generatedIds.getOrElse(idt, Set()).to(LazyList) case CallInfoType() => ??? @@ -1298,9 +1295,13 @@ object Interpreter { prog.findDatatype(name) match { case Some(dt1) => val dt = dt1.instantiate(typeArgs) - val dval = result.value.asInstanceOf[DataTypeValue] - val c = dt.dataTypeCases.find(_.name.name == dval.operationName).get - extractIdsList(dval.args, c.params.map(_.typ), prog) + result.value match { + case dval: DataTypeValue => + val c = dt.dataTypeCases.find(_.name.name == dval.operationName).get + extractIdsList(dval.args, c.params.map(_.typ), prog) + case other => + throw new Exception(s"Cannot extract ids from ${other} (${other.getClass})") + } case None => Map() } diff --git a/jvm/src/main/scala/crdtver/testing/RandomTester.scala b/jvm/src/main/scala/crdtver/testing/RandomTester.scala index 25fd2de..ec8f13b 100644 --- a/jvm/src/main/scala/crdtver/testing/RandomTester.scala +++ b/jvm/src/main/scala/crdtver/testing/RandomTester.scala @@ -205,10 +205,32 @@ class RandomTester(prog: InProgram, runArgs: RunArgs) { def randomValue(typ: InTypeExpr, knownIds: Map[IdType, Map[AnyValue, InvocationId]]): Option[AnyValue] = { typ match { case SimpleType(name, typeArgs) => - // TODO handle datatypes - // TODO substitute typeArgs - // don't generate value '0' as this is the initial value for registers - Some(Interpreter.domainValue(name, 1 + rand.nextInt(domainSize - 1))) + def randomDomainValue = { + // don't generate value '0' as this is the initial value for registers + Some(Interpreter.domainValue(name, 1 + rand.nextInt(domainSize - 1))) + } + + prog.findDatatype(name) match { + case None => + randomDomainValue + case Some(dtU) => + val dt = dtU.instantiate(typeArgs) + if (dt.dataTypeCases.isEmpty) + randomDomainValue + else { + val dtCase = pickRandom(dt.dataTypeCases)(rand) + val args = + for (param <- dtCase.params) yield { + randomValue(param.typ, knownIds) match { + case Some(v) => + v + case None => + return None + } + } + Some(AnyValue(DataTypeValue(dtCase.name.name, args))) + } + } case idt@IdType(_name) => knownIds.get(idt) match { case Some(s) => From eaeb060a06b71b1de4275ca77f82bbd13fa1258b Mon Sep 17 00:00:00 2001 From: Peter Zeller Date: Tue, 26 Jan 2021 23:35:51 +0100 Subject: [PATCH 04/10] fix typecheck issue helper always used the operation type, but here we want to create a datatype of the type T used inside the register --- .../language/crdts/MVRegisterCrdt.scala | 67 +++++++++++-------- 1 file changed, 39 insertions(+), 28 deletions(-) diff --git a/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala b/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala index 036fa92..5230d21 100644 --- a/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala +++ b/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala @@ -1,10 +1,10 @@ package crdtver.language.crdts +import crdtver.language.InputAst.{Identifier, NoSource} import crdtver.language.{TypedAst, crdts} -import crdtver.language.TypedAst.TypeVarUse +import crdtver.language.TypedAst.{FunctionKind, InExpr, TypeVarUse} import crdtver.language.TypedAstHelper._ import crdtver.language.crdts.ACrdtInstance.{QueryStructure, printTypes} -import crdtver.language.TypedAst.InExpr class MVRegisterCrdt extends CrdtTypeDefinition { @@ -138,59 +138,70 @@ class MVRegisterCrdt extends CrdtTypeDefinition { def _upperBoundedBy(val1: InExpr, val2: InExpr): InExpr = ( ( - val1 === makeOperation("R") && - (val2 === makeOperation("RW") || val2 === makeOperation("RX") || val2 === makeOperation("RWX")) + val1 === mkDatatypeCase("R") && + (val2 === mkDatatypeCase("RW") || val2 === mkDatatypeCase("RX") || val2 === mkDatatypeCase("RWX")) ) || ( - val1 === makeOperation("W") && - (val2 === makeOperation("RW") || val2 === makeOperation("WX") || val2 === makeOperation("RWX")) + val1 === mkDatatypeCase("W") && + (val2 === mkDatatypeCase("RW") || val2 === mkDatatypeCase("WX") || val2 === mkDatatypeCase("RWX")) ) || ( - val1 === makeOperation("X") && - (val2 === makeOperation("RX") || val2 === makeOperation("WX") || val2 === makeOperation("RWX")) + val1 === mkDatatypeCase("X") && + (val2 === mkDatatypeCase("RX") || val2 === mkDatatypeCase("WX") || val2 === mkDatatypeCase("RWX")) ) || ( - val1 === makeOperation("RW") && - (val2 === makeOperation("RWX")) + val1 === mkDatatypeCase("RW") && + (val2 === mkDatatypeCase("RWX")) ) || ( - val1 === makeOperation("RX") && - (val2 === makeOperation("RWX")) + val1 === mkDatatypeCase("RX") && + (val2 === mkDatatypeCase("RWX")) ) || ( - val1 === makeOperation("WX") && - (val2 === makeOperation("RWX")) + val1 === mkDatatypeCase("WX") && + (val2 === mkDatatypeCase("RWX")) ) ) + /** datatype constructor of type T (type of elements in the register) */ + private def mkDatatypeCase(name: String, args: TypedAst.InExpr*): TypedAst.FunctionCall = + TypedAst.FunctionCall( + source = NoSource(), + typ = T, + functionName = Identifier(NoSource(), name), + typeArgs = List(), + args = args.toList, + kind = FunctionKind.FunctionKindDatatypeConstructor() + ) + def _upperBoundedByOrEq(val1: InExpr, val2: InExpr): InExpr = ( ( - val1 === makeOperation("R") && - (val2 === makeOperation("R") || val2 === makeOperation("RW") || val2 === makeOperation("RX") || val2 === makeOperation("RWX")) + val1 === mkDatatypeCase("R") && + (val2 === mkDatatypeCase("R") || val2 === mkDatatypeCase("RW") || val2 === mkDatatypeCase("RX") || val2 === mkDatatypeCase("RWX")) ) || ( - val1 === makeOperation("W") && - (val2 === makeOperation("W") || val2 === makeOperation("RW") || val2 === makeOperation("WX") || val2 === makeOperation("RWX")) + val1 === mkDatatypeCase("W") && + (val2 === mkDatatypeCase("W") || val2 === mkDatatypeCase("RW") || val2 === mkDatatypeCase("WX") || val2 === mkDatatypeCase("RWX")) ) || ( - val1 === makeOperation("X") && - (val2 === makeOperation("X") || val2 === makeOperation("RX") || val2 === makeOperation("WX") || val2 === makeOperation("RWX")) + val1 === mkDatatypeCase("X") && + (val2 === mkDatatypeCase("X") || val2 === mkDatatypeCase("RX") || val2 === mkDatatypeCase("WX") || val2 === mkDatatypeCase("RWX")) ) || ( - val1 === makeOperation("RW") && - (val2 === makeOperation("RW") || val2 === makeOperation("RWX")) + val1 === mkDatatypeCase("RW") && + (val2 === mkDatatypeCase("RW") || val2 === mkDatatypeCase("RWX")) ) || ( - val1 === makeOperation("RX") && - (val2 === makeOperation("RX") || val2 === makeOperation("RWX")) + val1 === mkDatatypeCase("RX") && + (val2 === mkDatatypeCase("RX") || val2 === mkDatatypeCase("RWX")) ) || ( - val1 === makeOperation("WX") && - (val2 === makeOperation("WX") || val2 === makeOperation("RWX")) + val1 === mkDatatypeCase("WX") && + (val2 === mkDatatypeCase("WX") || val2 === mkDatatypeCase("RWX")) ) || ( - val1 === makeOperation("RWX") && - val2 === makeOperation("RWX") + val1 === mkDatatypeCase("RWX") && + val2 === mkDatatypeCase("RWX") ) ) } From 80f9d41644956ab818df95af995720256fc61f6a Mon Sep 17 00:00:00 2001 From: Michael Youssef Date: Wed, 27 Jan 2021 04:13:08 +0100 Subject: [PATCH 05/10] adjust crdt def --- .../language/crdts/MVRegisterCrdt.scala | 139 ++++++++++++++++-- 1 file changed, 123 insertions(+), 16 deletions(-) diff --git a/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala b/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala index 5230d21..18bd177 100644 --- 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( @@ -103,24 +107,86 @@ class MVRegisterCrdt extends CrdtTypeDefinition { // all uninterrupted Assigns to the register ) --> ( - (_upperBoundedByOrEq(someAssign, result)) && // upper bound + (_upperBoundedByOrEq(someAssign, result))// upper bound + ) + )) && + ( + forall(result2, + ( + forall(relevantCall2, forall(someAssign2, ( - 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)))) - ) --> - ( - _upperBoundedByOrEq(someValue2, result2) - ) - ))) --> - ( - _upperBoundedBy(result, result2) - ) + relevantCall2.isVis + && relevantCall2.op === makeOp(Assign, someAssign2) + && not(exists(otherCall2, exists(someValue2, otherCall2.isVis && relevantCall2 < otherCall2 && otherCall2.op === makeOp(Assign, someValue2)))) + ) --> + ( + _upperBoundedByOrEq(someAssign2, result2) ) + )) + ) --> + ( + _upperBoundedByOrEq(result, result2) + )) + ) + }), + 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) @@ -175,6 +241,11 @@ class MVRegisterCrdt extends CrdtTypeDefinition { ) def _upperBoundedByOrEq(val1: InExpr, val2: InExpr): InExpr = ( + ( + val1 === mkDatatypeCase("None") && + (val2 === mkDatatypeCase("None") || val2 === mkDatatypeCase("R") || val2 === mkDatatypeCase("W") || val2 === mkDatatypeCase("X") + || val2 === mkDatatypeCase("RW") || val2 === mkDatatypeCase("RX") || val2 === mkDatatypeCase("WX") || val2 === mkDatatypeCase("RWX")) + ) || ( val1 === mkDatatypeCase("R") && (val2 === mkDatatypeCase("R") || val2 === mkDatatypeCase("RW") || val2 === mkDatatypeCase("RX") || val2 === mkDatatypeCase("RWX")) @@ -204,6 +275,42 @@ class MVRegisterCrdt extends CrdtTypeDefinition { val2 === mkDatatypeCase("RWX") ) ) + + def _lowerBoundedByOrEq(val1: InExpr, val2: InExpr): InExpr = ( + ( + val1 === mkDatatypeCase("None") && + val2 === mkDatatypeCase("None") + ) || + ( + val1 === mkDatatypeCase("R") && + (val2 === mkDatatypeCase("None") || val2 === mkDatatypeCase("R")) + ) || + ( + val1 === mkDatatypeCase("W") && + (val2 === mkDatatypeCase("None") || val2 === mkDatatypeCase("W")) + ) || + ( + val1 === mkDatatypeCase("X") && + (val2 === mkDatatypeCase("None") || val2 === mkDatatypeCase("X")) + ) || + ( + val1 === mkDatatypeCase("RW") && + (val2 === mkDatatypeCase("None") || val2 === mkDatatypeCase("R") || val2 === mkDatatypeCase("W") || val2 === mkDatatypeCase("RW")) + ) || + ( + val1 === mkDatatypeCase("RX") && + (val2 === mkDatatypeCase("None") || val2 === mkDatatypeCase("R") || val2 === mkDatatypeCase("X") || val2 === mkDatatypeCase("RX")) + ) || + ( + val1 === mkDatatypeCase("WX") && + (val2 === mkDatatypeCase("None") || val2 === mkDatatypeCase("W") || val2 === mkDatatypeCase("X") || val2 === mkDatatypeCase("WX")) + ) || + ( + val1 === mkDatatypeCase("RWX") && + (val2 === mkDatatypeCase("None") || val2 === mkDatatypeCase("R") || val2 === mkDatatypeCase("W") || val2 === mkDatatypeCase("X") || val2 === mkDatatypeCase("RW") + || val2 === mkDatatypeCase("RX") || val2 === mkDatatypeCase("WX") || val2 === mkDatatypeCase("RWX")) + ) + ) } /** name of the CRDT */ From cd657cd52d7f8e56f302c2ff3842cfcc5c8e694d Mon Sep 17 00:00:00 2001 From: Michael Youssef Date: Thu, 28 Jan 2021 05:04:35 +0100 Subject: [PATCH 06/10] add file access rights crdt --- .../crdtver/language/TypedAstHelper.scala | 11 + .../language/crdts/CrdtTypeDefinition.scala | 1 + .../language/crdts/FileAccessCrdt.scala | 148 ---------- .../language/crdts/FileAccessRightsCrdt.scala | 254 ++++++++++++++++++ .../language/crdts/MVRegisterCrdt.scala | 2 +- 5 files changed, 267 insertions(+), 149 deletions(-) delete mode 100644 jvm/src/main/scala/crdtver/language/crdts/FileAccessCrdt.scala create mode 100644 jvm/src/main/scala/crdtver/language/crdts/FileAccessRightsCrdt.scala diff --git a/jvm/src/main/scala/crdtver/language/TypedAstHelper.scala b/jvm/src/main/scala/crdtver/language/TypedAstHelper.scala index fbfb539..94bc3e6 100644 --- a/jvm/src/main/scala/crdtver/language/TypedAstHelper.scala +++ b/jvm/src/main/scala/crdtver/language/TypedAstHelper.scala @@ -295,6 +295,17 @@ object TypedAstHelper { ) } + /** datatype constructor of type T (type of elements in the register) */ + def mkDatatypeCase(name: String, dtype: TypedAst.InTypeExpr, args: TypedAst.InExpr*): TypedAst.FunctionCall = + TypedAst.FunctionCall( + source = NoSource(), + typ = dtype, + functionName = Identifier(NoSource(), name), + typeArgs = List(), + args = args.toList, + kind = FunctionKind.FunctionKindDatatypeConstructor() + ) + // def makeOperation(name: String, operationType: InTypeExpr, tArgs: List[InTypeExpr], exp: TypedAst.InExpr*): TypedAst.FunctionCall = // makeOperationL(name, operationType, tArgs, exp.toList) diff --git a/jvm/src/main/scala/crdtver/language/crdts/CrdtTypeDefinition.scala b/jvm/src/main/scala/crdtver/language/crdts/CrdtTypeDefinition.scala index 793eedb..96a7cd1 100644 --- a/jvm/src/main/scala/crdtver/language/crdts/CrdtTypeDefinition.scala +++ b/jvm/src/main/scala/crdtver/language/crdts/CrdtTypeDefinition.scala @@ -82,6 +82,7 @@ object CrdtTypeDefinition { new MapCrdt(DW(), MapCrdt.DeleteAffectsPriorAndConcurrent(), "Map_dw"), new RegisterCrdt, new MVRegisterCrdt, + new FileAccessRightsCrdt, new CounterCrdt ) diff --git a/jvm/src/main/scala/crdtver/language/crdts/FileAccessCrdt.scala b/jvm/src/main/scala/crdtver/language/crdts/FileAccessCrdt.scala deleted file mode 100644 index 68bd2b8..0000000 --- a/jvm/src/main/scala/crdtver/language/crdts/FileAccessCrdt.scala +++ /dev/null @@ -1,148 +0,0 @@ -// package crdtver.language.crdts - -// import crdtver.language.TypedAst -// import crdtver.language.TypedAst.{BoolType, TypeVarUse} -// import crdtver.language.TypedAstHelper._ -// import crdtver.language.crdts.ACrdtInstance.{QueryStructure, printTypes} -// import crdtver.language.crdts.FlagCrdt.Strategy - -// class FileAccessCrdt extends CrdtTypeDefinition { - -// /** number of normal type parameters */ -// override def numberTypes: Int = 2 - -// /** number of CRDT type parameters */ -// override def numberInstances: Int = 0 - -// private val FAOp = "FAOp" - -// private val Assign = "Assign" - -// private val FAQry = "FAQry" - -// private val ReadFA = "ReadFA" - -// // predefined values for access rights -// private val None : TypedAst.InExpr = "None" // here is the problem, i cant define a InExpr type with single value for comparison in Strutegy - -// private val R : TypedAst.InExpr = "R" // here is the problem - -// private val W = "W" - -// private val X = "X" - -// private val RW = "RW" - -// private val RX = "RX" - -// private val WX = "WX" - -// private val RWX = "RWX" - -// // predefined values for user types - -// private val Admin = "Admin" - -// private val User = "User" - - -// override def additionalDataTypes: List[TypedAst.InTypeDecl] = List( -// dataType( -// FAOp, -// List("U", "V"), -// List( -// dtCase(Assign, List("user" -> TypeVarUse("U")(), "value" -> TypeVarUse("V")())) -// ) -// ), -// dataType(FAQry, List("V"), List(dtCase(ReadFA, List()))) -// ) - -// override def instantiate(typeArgs: List[TypedAst.InTypeExpr], crdtArgs: List[ACrdtInstance]): ACrdtInstance = new ACrdtInstance { -// val U: TypedAst.InTypeExpr = typeArgs.head // it should be User -// val V: TypedAst.InTypeExpr = (typeArgs.tail).head // make sure it will give the second item in list which must be Value - -// override def toString: String = s"${FileAccessCrdt.this.name}${printTypes(typeArgs, crdtArgs)}" - -// override def operationType: TypedAst.InTypeExpr = TypedAst.SimpleType(FAOp, List(U, V))() - -// override def queryType: TypedAst.InTypeExpr = TypedAst.SimpleType(FAQry, List(U, V))() - -// override def queryReturnType(q: QueryStructure): TypedAst.InTypeExpr = q match { -// case QueryStructure(ReadFA, List()) => V -// } - -// override def queryDefinitions(): List[TypedAst.InQueryDecl] = List( -// queryDeclEnsures(ReadFA, List(), V, { -// val result = varUse("result", V) -// val user1 = varUse("user1", U) -// val c = varUse("c") -// val c2 = varUse("c2") -// val v = varUse("v", V) -// val user2 = varUse("user2", U) -// not(exists(v, v !== None || v !== R || v !== W || v !== X || v !== RW || v !== RX || v !== WX || v !== RWX )) -// && -// not(exists(result, result !== None || result !== R || result !== W || result !== X || result !== RW || result !== RX || result !== WX || result !== RWX )) -// && -// not(exists(user1, user1 !== Admin || user1 !== User)) -// && -// not(exists(user2, user2 !== Admin || user2 !== User)) -// && - -// ( -// not(exists(c, exists(v, c.isVis && c.op === makeOp(Assign, user2, v) && user2 === Admin))) || -// ( -// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === R -// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && v === None -// ))) -// ) -// && -// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === W -// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && v === None //(v === None || v === R) -// ))) -// ) -// && -// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === E -// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && v === None //(v === None || v === R) -// ))) -// ) -// && -// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === RW -// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && (v === None || v === R || v === W ) -// ))) -// ) -// && -// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === RX -// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && (v === None || v === X || v === R ) -// ))) -// ) -// && -// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === WX -// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && (v === None || v === X || v === W ) -// ))) -// ) -// && -// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === Admin && result === RWX -// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin && c < c2 && (v === None || v === R || v === W || X) -// ))) -// ) -// ) -// ) - -// && -// ( -// exists(c, c.isVis && c.op === makeOp(Assign, user1, result) && user1 === User -// && not(exists(c2, exists(v, c2.isVis && c2.op === makeOp(Assign, user2, v) && user2 === Admin -// ))) -// ) -// ) - -// }) - -// ) - -// override def additionalDataTypesRec: List[TypedAst.InTypeDecl] = FileAccessCrdt.this.additionalDataTypes -// } - -// /** name of the CRDT */ -// override def name: String = "FileAccessTuple" -// } diff --git a/jvm/src/main/scala/crdtver/language/crdts/FileAccessRightsCrdt.scala b/jvm/src/main/scala/crdtver/language/crdts/FileAccessRightsCrdt.scala new file mode 100644 index 0000000..a26b3ac --- /dev/null +++ b/jvm/src/main/scala/crdtver/language/crdts/FileAccessRightsCrdt.scala @@ -0,0 +1,254 @@ +package crdtver.language.crdts + +import crdtver.language.InputAst.{Identifier, NoSource} +import crdtver.language.{TypedAst, crdts} +import crdtver.language.TypedAst.{FunctionKind, InExpr, TypeVarUse} +import crdtver.language.TypedAstHelper._ +import crdtver.language.crdts.ACrdtInstance.{QueryStructure, printTypes} + + +class FileAccessRightsCrdt extends CrdtTypeDefinition { + + /** number of normal type parameters */ + override def numberTypes: Int = 1 + + /** number of CRDT type parameters */ + override def numberInstances: Int = 0 + + private val FileAccessRightsQry = "FileAccessRightsQry" + + private val RegisterOp = "RegisterOp" + + private val Assign = "Assign" + + private val ReadPermsUB = "ReadPermsUB" + + private val ReadPermsLB = "ReadPermsLB" + + + override def additionalDataTypes: List[TypedAst.InTypeDecl] = List( + dataType( + RegisterOp, + List("T"), + List( + dtCase(Assign, List("value" -> TypeVarUse("T")())), + ) + ), + dataType(FileAccessRightsQry, List("T"),List( + dtCase(ReadPermsUB, List()), + dtCase(ReadPermsLB, List()) + ))) + + override def instantiate(typeArgs: List[TypedAst.InTypeExpr], crdtArgs: List[ACrdtInstance]): ACrdtInstance = new ACrdtInstance { + + override def toString: String = s"${FileAccessRightsCrdt.this.name}${printTypes(typeArgs, crdtArgs)}" + + val T: TypedAst.InTypeExpr = typeArgs.head + + override def operationType: TypedAst.InTypeExpr = TypedAst.SimpleType(RegisterOp, List(T))() + + override def queryType: TypedAst.InTypeExpr = TypedAst.SimpleType(FileAccessRightsQry, List(T))() + + override def queryReturnType(q: QueryStructure): TypedAst.InTypeExpr = q match { + case QueryStructure(ReadPermsUB, List()) => T + case QueryStructure(ReadPermsLB, List()) => T + } + + override def queryDefinitions(): List[TypedAst.InQueryDecl] = List( + queryDeclEnsures(ReadPermsUB, 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(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)))) + ) --> + ( + _upperBoundedByOrEq(someAssign2, result2) + ) + )) + ) --> + ( + _upperBoundedByOrEq(result, result2) + )) + ) + }), + queryDeclEnsures(ReadPermsLB, 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 + ) --> + ( + (_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) + )) + ) + }) + ) + + override def additionalDataTypesRec: List[TypedAst.InTypeDecl] = FileAccessRightsCrdt.this.additionalDataTypes + + def _upperBoundedBy(val1: InExpr, val2: InExpr): InExpr = ( + ( + val1 === mkDatatypeCase("R", T) && + (val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("W", T) && + (val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("X", T) && + (val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("RW", T) && + (val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("RX", T) && + (val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("WX", T) && + (val2 === mkDatatypeCase("RWX", T)) + ) + ) + + def _upperBoundedByOrEq(val1: InExpr, val2: InExpr): InExpr = ( + ( + val1 === mkDatatypeCase("None", T) && + (val2 === mkDatatypeCase("None", T) || val2 === mkDatatypeCase("R", T) || val2 === mkDatatypeCase("W", T) || val2 === mkDatatypeCase("X", T) + || val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("R", T) && + (val2 === mkDatatypeCase("R", T) || val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("W", T) && + (val2 === mkDatatypeCase("W", T) || val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("X", T) && + (val2 === mkDatatypeCase("X", T) || val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("RW", T) && + (val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("RX", T) && + (val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("WX", T) && + (val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("RWX", T) && + val2 === mkDatatypeCase("RWX", T) + ) + ) + + def _lowerBoundedByOrEq(val1: InExpr, val2: InExpr): InExpr = ( + ( + val1 === mkDatatypeCase("None", T) && + val2 === mkDatatypeCase("None", T) + ) || + ( + val1 === mkDatatypeCase("R", T) && + (val2 === mkDatatypeCase("None", T) || val2 === mkDatatypeCase("R", T)) + ) || + ( + val1 === mkDatatypeCase("W", T) && + (val2 === mkDatatypeCase("None", T) || val2 === mkDatatypeCase("W", T)) + ) || + ( + val1 === mkDatatypeCase("X", T) && + (val2 === mkDatatypeCase("None", T) || val2 === mkDatatypeCase("X", T)) + ) || + ( + val1 === mkDatatypeCase("RW", T) && + (val2 === mkDatatypeCase("None", T) || val2 === mkDatatypeCase("R", T) || val2 === mkDatatypeCase("W", T) || val2 === mkDatatypeCase("RW", T)) + ) || + ( + val1 === mkDatatypeCase("RX", T) && + (val2 === mkDatatypeCase("None", T) || val2 === mkDatatypeCase("R", T) || val2 === mkDatatypeCase("X", T) || val2 === mkDatatypeCase("RX", T)) + ) || + ( + val1 === mkDatatypeCase("WX", T) && + (val2 === mkDatatypeCase("None", T) || val2 === mkDatatypeCase("W", T) || val2 === mkDatatypeCase("X", T) || val2 === mkDatatypeCase("WX", T)) + ) || + ( + val1 === mkDatatypeCase("RWX", T) && + (val2 === mkDatatypeCase("None", T) || val2 === mkDatatypeCase("R", T) || val2 === mkDatatypeCase("W", T) || val2 === mkDatatypeCase("X", T) || val2 === mkDatatypeCase("RW", T) + || val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + ) + ) + } + + /** name of the CRDT */ + override def name: String = "FileAccessRights" +} + diff --git a/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala b/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala index 18bd177..f0fe25d 100644 --- a/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala +++ b/jvm/src/main/scala/crdtver/language/crdts/MVRegisterCrdt.scala @@ -25,7 +25,7 @@ class MVRegisterCrdt extends CrdtTypeDefinition { private val ReadPermsUpper = "ReadPermsUpper" - private val ReadPermsLower = "ReadPermsLower " + private val ReadPermsLower = "ReadPermsLower" private val MvContains = "MvContains" From b6131c047630444957460a0019fce97eb67a1d04 Mon Sep 17 00:00:00 2001 From: Michael Youssef Date: Thu, 28 Jan 2021 23:57:29 +0100 Subject: [PATCH 07/10] add file access rights crdt w admin rights --- .../crdts/AFileAccessRightsCrdt.scala | 231 ++++++++++++++++++ .../language/crdts/CrdtTypeDefinition.scala | 1 + 2 files changed, 232 insertions(+) create mode 100644 jvm/src/main/scala/crdtver/language/crdts/AFileAccessRightsCrdt.scala diff --git a/jvm/src/main/scala/crdtver/language/crdts/AFileAccessRightsCrdt.scala b/jvm/src/main/scala/crdtver/language/crdts/AFileAccessRightsCrdt.scala new file mode 100644 index 0000000..ce2552a --- /dev/null +++ b/jvm/src/main/scala/crdtver/language/crdts/AFileAccessRightsCrdt.scala @@ -0,0 +1,231 @@ +package crdtver.language.crdts + +import crdtver.language.InputAst.{Identifier, NoSource} +import crdtver.language.{TypedAst, crdts} +import crdtver.language.TypedAst.{FunctionKind, InExpr, TypeVarUse} +import crdtver.language.TypedAstHelper._ +import crdtver.language.crdts.ACrdtInstance.{QueryStructure, printTypes} + + +class AFileAccessRightsCrdt extends CrdtTypeDefinition { + + /** number of normal type parameters */ + override def numberTypes: Int = 1 + + /** number of CRDT type parameters */ + override def numberInstances: Int = 0 + + private val AFileAccessRightsQry = "AFileAccessRightsQry" + + private val RegisterOp = "RegisterOp" + + private val Assign = "Assign" + + private val ReadPermsUB = "ReadPermsUB" + + private val ReadPermsLB = "ReadPermsLB" + + + override def additionalDataTypes: List[TypedAst.InTypeDecl] = List( + dataType( + RegisterOp, + List("T"), + List( + dtCase(Assign, List("value" -> TypeVarUse("T")())), + ) + ), + dataType(AFileAccessRightsQry, List("T"),List( + dtCase(ReadPermsUB, List()), + dtCase(ReadPermsLB, List()) + ))) + + override def instantiate(typeArgs: List[TypedAst.InTypeExpr], crdtArgs: List[ACrdtInstance]): ACrdtInstance = new ACrdtInstance { + + override def toString: String = s"${AFileAccessRightsCrdt.this.name}${printTypes(typeArgs, crdtArgs)}" + + val T: TypedAst.InTypeExpr = typeArgs.head + + override def operationType: TypedAst.InTypeExpr = TypedAst.SimpleType(RegisterOp, List(T))() + + override def queryType: TypedAst.InTypeExpr = TypedAst.SimpleType(AFileAccessRightsQry, List(T))() + + override def queryReturnType(q: QueryStructure): TypedAst.InTypeExpr = q match { + case QueryStructure(ReadPermsUB, List()) => T + case QueryStructure(ReadPermsLB, List()) => T + } + + override def queryDefinitions(): List[TypedAst.InQueryDecl] = List( + queryDeclEnsures(ReadPermsUB, 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(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)))) + ) --> + ( + _upperBoundedByOrEq(someAssign2, result2) + ) + )) + ) --> + ( + _upperBoundedByOrEq(result, result2) + )) + ) + }), + queryDeclEnsures(ReadPermsLB, 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 + ) --> + ( + (_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) + )) + ) + }) + ) + + override def additionalDataTypesRec: List[TypedAst.InTypeDecl] = AFileAccessRightsCrdt.this.additionalDataTypes + + // TODO: + def _upperBoundedByOrEq(val1: InExpr, val2: InExpr): InExpr = ( + ( + val1 === mkDatatypeCase("None", T) && + (val2 === mkDatatypeCase("None", T) || val2 === mkDatatypeCase("R", T) || val2 === mkDatatypeCase("W", T) || val2 === mkDatatypeCase("X", T) + || val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("R", T) && + (val2 === mkDatatypeCase("R", T) || val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("W", T) && + (val2 === mkDatatypeCase("W", T) || val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("X", T) && + (val2 === mkDatatypeCase("X", T) || val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("RW", T) && + (val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("RX", T) && + (val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("WX", T) && + (val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + ) || + ( + val1 === mkDatatypeCase("RWX", T) && + val2 === mkDatatypeCase("RWX", T) + ) + ) + + def _lowerBoundedByOrEq(val1: InExpr, val2: InExpr): InExpr = ( + ( + val1 === mkDatatypeCase("ANone", T) && + val2 === mkDatatypeCase("ANone", T) + ) || + ( + val1 === mkDatatypeCase("AR", T) && + (val2 === mkDatatypeCase("ANone", T) || val2 === mkDatatypeCase("AR", T)) + ) || + ( + val1 === mkDatatypeCase("AW", T) && + (val2 === mkDatatypeCase("ANone", T) || val2 === mkDatatypeCase("AW", T)) + ) || + ( + val1 === mkDatatypeCase("ARW", T) && + (val2 === mkDatatypeCase("ANone", T) || val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) || val2 === mkDatatypeCase("ARW", T)) + ) || + ( + val1 === mkDatatypeCase("UNone", T) && + (val2 === mkDatatypeCase("UNone", T) || val2 === mkDatatypeCase("ARW", T) || val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) + ||val2 === mkDatatypeCase("ANone", T)) + ) || + ( + val1 === mkDatatypeCase("UR", T) && + (val2 === mkDatatypeCase("UR", T) || val2 === mkDatatypeCase("UNone", T) || val2 === mkDatatypeCase("ARW", T) || val2 === mkDatatypeCase("AR", T) + || val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T)) + ) || + ( + val1 === mkDatatypeCase("UW", T) && + (val2 === mkDatatypeCase("UW", T) || val2 === mkDatatypeCase("UNone", T) || val2 === mkDatatypeCase("ARW", T) || val2 === mkDatatypeCase("AR", T) + || val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T)) + ) || + ( + val1 === mkDatatypeCase("URW", T) && + ( val2 === mkDatatypeCase("URW", T) || val2 === mkDatatypeCase("UR", T) || val2 === mkDatatypeCase("UW", T) || val2 === mkDatatypeCase("UNone", T) + || val2 === mkDatatypeCase("ARW", T) || val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T)) + ) + ) + } + + /** name of the CRDT */ + override def name: String = "AFileAccessRights" +} + diff --git a/jvm/src/main/scala/crdtver/language/crdts/CrdtTypeDefinition.scala b/jvm/src/main/scala/crdtver/language/crdts/CrdtTypeDefinition.scala index 96a7cd1..e23b921 100644 --- a/jvm/src/main/scala/crdtver/language/crdts/CrdtTypeDefinition.scala +++ b/jvm/src/main/scala/crdtver/language/crdts/CrdtTypeDefinition.scala @@ -83,6 +83,7 @@ object CrdtTypeDefinition { new RegisterCrdt, new MVRegisterCrdt, new FileAccessRightsCrdt, + new AFileAccessRightsCrdt, new CounterCrdt ) From 8c55a2b8968c265b0ebd0a1b6dc754dea07255e7 Mon Sep 17 00:00:00 2001 From: Michael Youssef Date: Sat, 30 Jan 2021 23:12:11 +0100 Subject: [PATCH 08/10] add test --- .../test/scala/repliss/InterpreterTests.scala | 220 ++++++++++++++---- 1 file changed, 172 insertions(+), 48 deletions(-) diff --git a/jvm/src/test/scala/repliss/InterpreterTests.scala b/jvm/src/test/scala/repliss/InterpreterTests.scala index 2216573..145c888 100644 --- a/jvm/src/test/scala/repliss/InterpreterTests.scala +++ b/jvm/src/test/scala/repliss/InterpreterTests.scala @@ -2,7 +2,7 @@ package repliss import crdtver.Repliss.{Quickcheck, ReplissResult} import crdtver.testing.Interpreter -import crdtver.testing.Interpreter.{AnyValue, CallAction, InvariantCheck, InvariantViolationException, InvocationId, LocalAction, NewId, Return, StartTransaction, TransactionId, domainValue} +import crdtver.testing.Interpreter.{AnyValue, DataTypeValue, CallAction, InvariantCheck, InvariantViolationException, InvocationId, LocalAction, NewId, Return, StartTransaction, TransactionId, domainValue} import crdtver.utils.Helper import crdtver.{Repliss, RunArgs} import org.scalatest.funsuite.AnyFunSuite @@ -17,44 +17,137 @@ class InterpreterTests extends AnyFunSuite with Matchers { - test("find chatapp example") { - - val prog = Repliss.parseAndTypecheck("chatapp", Helper.getResource("/examples/buggy/chatapp_fail1.rpls")).get() +// test("find chatapp example") { + +// val prog = Repliss.parseAndTypecheck("chatapp", Helper.getResource("/examples/buggy/chatapp_fail1.rpls")).get() +// val i = new Interpreter(prog, RunArgs(), domainSize = 3) +// var s = Interpreter.State() +// val i1 = InvocationId(1) +// val i2 = InvocationId(2) +// val i3 = InvocationId(3) +// val i4 = InvocationId(4) +// val i5 = InvocationId(5) +// val t1 = TransactionId(1) +// val t2 = TransactionId(2) +// val t3 = TransactionId(3) +// val t4 = TransactionId(4) + +// // [info] 0. invoc_1 call sendMessage(UserId_1, String_0) +// // [info] 1. invoc_1 startTx() => tx_1 +// // [info] 2. invoc_1 newId(0) +// // [info] 3. invoc_1 return +// // [info] 4. invoc_2 call editMessage(MessageId_000, String_0) +// // [info] 5. invoc_2 startTx() => tx_2 +// // [info] 6. invoc_2 return +// // [info] 7. invoc_3 call deleteMessage(MessageId_000) +// // [info] 8. invoc_3 startTx() => tx_3 +// // [info] 9. invoc_3 return +// // [info] 10. invoc_4 call getMessage(MessageId_000) +// // [info] 11. invoc_4 startTx(tx_2, tx_3) => tx_4 +// // [info] 12. invoc_4 return + +// val user1 = domainValue("UserId", 1) +// val string0 = domainValue("String", 0) +// val string1 = domainValue("String", 1) +// val message1 =domainValue("MessageId", 1) + +// s = i.executeAction(s, CallAction(i1, "sendMessage", List(user1, string0))).get +// s = i.executeAction(s, LocalAction(i1, StartTransaction(t1, Set()))).get +// s = i.executeAction(s, LocalAction(i1, NewId(1))).get +// s = i.executeAction(s, LocalAction(i1, Return())).get + +// println(s"knownIds = ${s.knownIds}") + +// for (k <- s.knownIds.values; kk <- k.keys) { +// println(s"Id = $kk (${kk.value.getClass})") +// } + +// s = i.executeAction(s, CallAction(i2, "editMessage", List(message1, string1))).get +// s = i.executeAction(s, LocalAction(i2, StartTransaction(t2, Set()))).get +// s = i.executeAction(s, LocalAction(i2, Return())).get + +// s = i.executeAction(s, CallAction(i3, "deleteMessage", List(message1))).get +// s = i.executeAction(s, LocalAction(i3, StartTransaction(t3, Set()))).get +// s = i.executeAction(s, LocalAction(i3, Return())).get + +// s = i.executeAction(s, CallAction(i4, "getMessage", List(message1))).get +// s = i.executeAction(s, LocalAction(i4, StartTransaction(t4, Set(t2, t3)))).get +// s = i.executeAction(s, LocalAction(i4, Return())).get + +// // s = i.executeAction(s, CallAction(i5, "getMessage", List(AnyValue("MessageId_001")))).get +// try { +// i.checkInvariants(s) +// // s = i.executeAction(s, InvariantCheck(i5)).get +// fail("Invariant-check should fail") +// } catch { +// case iv: InvariantViolationException => +// println(iv) +// for (info <- iv.info) +// println(info) +// } + +// } + + + test("file_system") { + + val prog = Repliss.parseAndTypecheck("fs", Helper.getResource("/examples/buggy/fs.rpls")).get() val i = new Interpreter(prog, RunArgs(), domainSize = 3) var s = Interpreter.State() - val i1 = InvocationId(1) - val i2 = InvocationId(2) - val i3 = InvocationId(3) - val i4 = InvocationId(4) - val i5 = InvocationId(5) - val t1 = TransactionId(1) - val t2 = TransactionId(2) - val t3 = TransactionId(3) - val t4 = TransactionId(4) - -// [info] 0. invoc_1 call sendMessage(UserId_1, String_0) -// [info] 1. invoc_1 startTx() => tx_1 -// [info] 2. invoc_1 newId(0) -// [info] 3. invoc_1 return -// [info] 4. invoc_2 call editMessage(MessageId_000, String_0) -// [info] 5. invoc_2 startTx() => tx_2 -// [info] 6. invoc_2 return -// [info] 7. invoc_3 call deleteMessage(MessageId_000) -// [info] 8. invoc_3 startTx() => tx_3 -// [info] 9. invoc_3 return -// [info] 10. invoc_4 call getMessage(MessageId_000) -// [info] 11. invoc_4 startTx(tx_2, tx_3) => tx_4 -// [info] 12. invoc_4 return - - val user1 = domainValue("UserId", 1) - val string0 = domainValue("String", 0) - val string1 = domainValue("String", 1) - val message1 =domainValue("MessageId", 1) - - s = i.executeAction(s, CallAction(i1, "sendMessage", List(user1, string0))).get - s = i.executeAction(s, LocalAction(i1, StartTransaction(t1, Set()))).get - s = i.executeAction(s, LocalAction(i1, NewId(1))).get - s = i.executeAction(s, LocalAction(i1, Return())).get + + val createAdminInvocId = InvocationId(1); + val createUserInvocId = InvocationId(2); + val createGroupInvocId = InvocationId(3); + val assignToGroupInvocId = InvocationId(4); + val createFileInvocId = InvocationId(5); + val changeOwnerInvocId = InvocationId(6); + val changeOwnerPermsInvocId = InvocationId(7); + val readFileInvocId = InvocationId(8); + + + val createAdminTrasnactionId = TransactionId(1); + val createUserTrasnactionId = TransactionId(2); + val createGroupTransactionId = TransactionId(3); + val assignToGroupTransactionId = TransactionId(4); + val createFileTrasnactionId = TransactionId(5); + val changeOwnerTrasnactionId = TransactionId(6); + val changeOwnerPermsTrasnactionId = TransactionId(7); + val readFileTrasnactionId = TransactionId(8); + + + val admin1 = domainValue("UserId", 1); + val user1 = domainValue("UserId", 2); + val file1 = domainValue("NodeId", 1); + val group1 = domainValue("GroupId", 1); + val writAccessRight = AnyValue(DataTypeValue("UW", List())); + + // create admin + s = i.executeAction(s, CallAction(createAdminInvocId, "createUser", List(AnyValue(true)))).get // create admin + s = i.executeAction(s, LocalAction(createAdminInvocId, StartTransaction(createAdminTrasnactionId, Set()))).get + s = i.executeAction(s, LocalAction(createAdminInvocId, NewId(1))).get + s = i.executeAction(s, LocalAction(createAdminInvocId, Return())).get + println(s"admin created"); + + // create user + s = i.executeAction(s, CallAction(createUserInvocId, "createUser", List(AnyValue(false)))).get // create admin + s = i.executeAction(s, LocalAction(createUserInvocId, StartTransaction(createUserTrasnactionId, Set()))).get + s = i.executeAction(s, LocalAction(createUserInvocId, NewId(2))).get + s = i.executeAction(s, LocalAction(createUserInvocId, Return())).get + println(s"user created"); + + // create group + s = i.executeAction(s, CallAction(createGroupInvocId, "createGroup", List())).get // create admin + s = i.executeAction(s, LocalAction(createGroupInvocId, StartTransaction(createGroupTransactionId, Set()))).get + s = i.executeAction(s, LocalAction(createGroupInvocId, NewId(1))).get + s = i.executeAction(s, LocalAction(createGroupInvocId, Return())).get + println("Group created") + + // assign user to group + s = i.executeAction(s, CallAction(assignToGroupInvocId, "assignUserToGroup", List(admin1, group1, user1))).get + s = i.executeAction(s, LocalAction(assignToGroupInvocId, StartTransaction(assignToGroupTransactionId, Set(createUserTrasnactionId, createAdminTrasnactionId)))).get + s = i.executeAction(s, LocalAction(assignToGroupInvocId, Return())).get + println(s"user assigned to group"); + println(s"knownIds = ${s.knownIds}") @@ -62,17 +155,48 @@ class InterpreterTests extends AnyFunSuite with Matchers { println(s"Id = $kk (${kk.value.getClass})") } - s = i.executeAction(s, CallAction(i2, "editMessage", List(message1, string1))).get - s = i.executeAction(s, LocalAction(i2, StartTransaction(t2, Set()))).get - s = i.executeAction(s, LocalAction(i2, Return())).get - - s = i.executeAction(s, CallAction(i3, "deleteMessage", List(message1))).get - s = i.executeAction(s, LocalAction(i3, StartTransaction(t3, Set()))).get - s = i.executeAction(s, LocalAction(i3, Return())).get - - s = i.executeAction(s, CallAction(i4, "getMessage", List(message1))).get - s = i.executeAction(s, LocalAction(i4, StartTransaction(t4, Set(t2, t3)))).get - s = i.executeAction(s, LocalAction(i4, Return())).get + // create file + s = i.executeAction(s, CallAction(createFileInvocId, "createFile", List(user1, group1))).get + s = i.executeAction(s, LocalAction(createFileInvocId, StartTransaction(createFileTrasnactionId, Set(createAdminTrasnactionId, assignToGroupTransactionId)))).get + s = i.executeAction(s, LocalAction(createFileInvocId, NewId(1))).get + s = i.executeAction(s, LocalAction(createFileInvocId, Return())).get + println(s"file created"); + + // change owner of file + s = i.executeAction(s, CallAction(changeOwnerInvocId, "changeOwner", List(admin1, admin1, file1))).get + s = i.executeAction(s, LocalAction(changeOwnerInvocId, StartTransaction(changeOwnerTrasnactionId, Set(createFileTrasnactionId)))).get + s = i.executeAction(s, LocalAction(changeOwnerInvocId, Return())).get + println(s"owner changed"); + + // change owner perms//changeOwnerPermission(userId: UserId, newPermission: AccessRight, fileId: NodeId) + s = i.executeAction(s, CallAction(changeOwnerPermsInvocId, "changeOwnerPermission", List(user1, writAccessRight, file1))).get + s = i.executeAction(s, LocalAction(changeOwnerPermsInvocId, StartTransaction(changeOwnerPermsTrasnactionId, Set(createFileTrasnactionId)))).get + s = i.executeAction(s, LocalAction(changeOwnerPermsInvocId, Return())).get + println(s"owner perms changed"); + + // read + s = i.executeAction(s, CallAction(readFileInvocId, "readFile", List(user1, file1))).get + s = i.executeAction(s, LocalAction(readFileInvocId, StartTransaction(readFileTrasnactionId, Set(changeOwnerTrasnactionId, changeOwnerPermsTrasnactionId)))).get + s = i.executeAction(s, LocalAction(readFileInvocId, Return())).get + println(s"done"); + + // println(s"knownIds = ${s.knownIds}") + + // for (k <- s.knownIds.values; kk <- k.keys) { + // println(s"Id = $kk (${kk.value.getClass})") + // } + + // s = i.executeAction(s, CallAction(i2, "editMessage", List(message1, string1))).get + // s = i.executeAction(s, LocalAction(i2, StartTransaction(t2, Set()))).get + // s = i.executeAction(s, LocalAction(i2, Return())).get + + // s = i.executeAction(s, CallAction(i3, "deleteMessage", List(message1))).get + // s = i.executeAction(s, LocalAction(i3, StartTransaction(t3, Set()))).get + // s = i.executeAction(s, LocalAction(i3, Return())).get + + // s = i.executeAction(s, CallAction(i4, "getMessage", List(message1))).get + // s = i.executeAction(s, LocalAction(i4, StartTransaction(t4, Set(t2, t3)))).get + // s = i.executeAction(s, LocalAction(i4, Return())).get // s = i.executeAction(s, CallAction(i5, "getMessage", List(AnyValue("MessageId_001")))).get try { From 5bc568c497a057ef919a70085372e645f4ada087 Mon Sep 17 00:00:00 2001 From: Michael Youssef Date: Mon, 1 Feb 2021 12:26:46 +0100 Subject: [PATCH 09/10] add more tests --- .../test/scala/repliss/InterpreterTests.scala | 210 +++++++++++++++++- 1 file changed, 200 insertions(+), 10 deletions(-) diff --git a/jvm/src/test/scala/repliss/InterpreterTests.scala b/jvm/src/test/scala/repliss/InterpreterTests.scala index 145c888..10a3589 100644 --- a/jvm/src/test/scala/repliss/InterpreterTests.scala +++ b/jvm/src/test/scala/repliss/InterpreterTests.scala @@ -89,9 +89,9 @@ class InterpreterTests extends AnyFunSuite with Matchers { // } - test("file_system") { + test("file_system_fail1") { - val prog = Repliss.parseAndTypecheck("fs", Helper.getResource("/examples/buggy/fs.rpls")).get() + val prog = Repliss.parseAndTypecheck("fs", Helper.getResource("/examples/buggy/5.rpls")).get() val i = new Interpreter(prog, RunArgs(), domainSize = 3) var s = Interpreter.State() @@ -147,17 +147,10 @@ class InterpreterTests extends AnyFunSuite with Matchers { s = i.executeAction(s, LocalAction(assignToGroupInvocId, StartTransaction(assignToGroupTransactionId, Set(createUserTrasnactionId, createAdminTrasnactionId)))).get s = i.executeAction(s, LocalAction(assignToGroupInvocId, Return())).get println(s"user assigned to group"); - - - println(s"knownIds = ${s.knownIds}") - - for (k <- s.knownIds.values; kk <- k.keys) { - println(s"Id = $kk (${kk.value.getClass})") - } // create file s = i.executeAction(s, CallAction(createFileInvocId, "createFile", List(user1, group1))).get - s = i.executeAction(s, LocalAction(createFileInvocId, StartTransaction(createFileTrasnactionId, Set(createAdminTrasnactionId, assignToGroupTransactionId)))).get + s = i.executeAction(s, LocalAction(createFileInvocId, StartTransaction(createFileTrasnactionId, Set(assignToGroupTransactionId)))).get s = i.executeAction(s, LocalAction(createFileInvocId, NewId(1))).get s = i.executeAction(s, LocalAction(createFileInvocId, Return())).get println(s"file created"); @@ -212,5 +205,202 @@ class InterpreterTests extends AnyFunSuite with Matchers { } + test("file_system_pass1") { + + val prog = Repliss.parseAndTypecheck("fs", Helper.getResource("/examples/buggy/5.rpls")).get() + val i = new Interpreter(prog, RunArgs(), domainSize = 3) + var s = Interpreter.State() + + val createAdminInvocId = InvocationId(1); + val createUserInvocId = InvocationId(2); + val createGroupInvocId = InvocationId(3); + val assignToGroupInvocId = InvocationId(4); + val createFileInvocId = InvocationId(5); + val changeOwnerInvocId = InvocationId(6); + val changeOwnerPermsInvocId = InvocationId(7); + val changeOwnerPermsInvocId2 = InvocationId(8); + val readFileInvocId = InvocationId(9); + + + val createAdminTrasnactionId = TransactionId(1); + val createUserTrasnactionId = TransactionId(2); + val createGroupTransactionId = TransactionId(3); + val assignToGroupTransactionId = TransactionId(4); + val createFileTrasnactionId = TransactionId(5); + val changeOwnerTrasnactionId = TransactionId(6); + val changeOwnerPermsTrasnactionId = TransactionId(7); + val changeOwnerPermsTrasnactionId2 = TransactionId(8); + val readFileTrasnactionId = TransactionId(9); + + + val admin1 = domainValue("UserId", 1); + val user1 = domainValue("UserId", 2); + val file1 = domainValue("NodeId", 1); + val group1 = domainValue("GroupId", 1); + val writeAccessRight = AnyValue(DataTypeValue("UW", List())); + val readWriteAccessRight = AnyValue(DataTypeValue("URW", List())); + + // create admin + s = i.executeAction(s, CallAction(createAdminInvocId, "createUser", List(AnyValue(true)))).get // create admin + s = i.executeAction(s, LocalAction(createAdminInvocId, StartTransaction(createAdminTrasnactionId, Set()))).get + s = i.executeAction(s, LocalAction(createAdminInvocId, NewId(1))).get + s = i.executeAction(s, LocalAction(createAdminInvocId, Return())).get + println(s"admin created"); + + // create user + s = i.executeAction(s, CallAction(createUserInvocId, "createUser", List(AnyValue(false)))).get // create admin + s = i.executeAction(s, LocalAction(createUserInvocId, StartTransaction(createUserTrasnactionId, Set()))).get + s = i.executeAction(s, LocalAction(createUserInvocId, NewId(2))).get + s = i.executeAction(s, LocalAction(createUserInvocId, Return())).get + println(s"user created"); + + // create group + s = i.executeAction(s, CallAction(createGroupInvocId, "createGroup", List())).get // create admin + s = i.executeAction(s, LocalAction(createGroupInvocId, StartTransaction(createGroupTransactionId, Set()))).get + s = i.executeAction(s, LocalAction(createGroupInvocId, NewId(1))).get + s = i.executeAction(s, LocalAction(createGroupInvocId, Return())).get + println("Group created") + + // assign user to group + s = i.executeAction(s, CallAction(assignToGroupInvocId, "assignUserToGroup", List(admin1, group1, user1))).get + s = i.executeAction(s, LocalAction(assignToGroupInvocId, StartTransaction(assignToGroupTransactionId, Set(createUserTrasnactionId, createAdminTrasnactionId)))).get + s = i.executeAction(s, LocalAction(assignToGroupInvocId, Return())).get + println(s"user assigned to group"); + + // create file + s = i.executeAction(s, CallAction(createFileInvocId, "createFile", List(user1, group1))).get + s = i.executeAction(s, LocalAction(createFileInvocId, StartTransaction(createFileTrasnactionId, Set(assignToGroupTransactionId)))).get + s = i.executeAction(s, LocalAction(createFileInvocId, NewId(1))).get + s = i.executeAction(s, LocalAction(createFileInvocId, Return())).get + println(s"file created"); + + // change owner of file + s = i.executeAction(s, CallAction(changeOwnerInvocId, "changeOwner", List(admin1, admin1, file1))).get + s = i.executeAction(s, LocalAction(changeOwnerInvocId, StartTransaction(changeOwnerTrasnactionId, Set(createFileTrasnactionId)))).get + s = i.executeAction(s, LocalAction(changeOwnerInvocId, Return())).get + println(s"owner changed"); + + // change owner perms + s = i.executeAction(s, CallAction(changeOwnerPermsInvocId, "changeOwnerPermission", List(user1, writeAccessRight, file1))).get + s = i.executeAction(s, LocalAction(changeOwnerPermsInvocId, StartTransaction(changeOwnerPermsTrasnactionId, Set(createFileTrasnactionId)))).get + s = i.executeAction(s, LocalAction(changeOwnerPermsInvocId, Return())).get + println(s"owner perms changed"); + + + // change owner perms + s = i.executeAction(s, CallAction(changeOwnerPermsInvocId2, "changeOwnerPermission", List(user1, readWriteAccessRight, file1))).get + s = i.executeAction(s, LocalAction(changeOwnerPermsInvocId2, StartTransaction(changeOwnerPermsTrasnactionId2, Set(changeOwnerPermsTrasnactionId)))).get + s = i.executeAction(s, LocalAction(changeOwnerPermsInvocId2, Return())).get + println(s"owner perms changed 2"); + + // read + s = i.executeAction(s, CallAction(readFileInvocId, "readFile", List(user1, file1))).get + s = i.executeAction(s, LocalAction(readFileInvocId, StartTransaction(readFileTrasnactionId, Set(changeOwnerTrasnactionId, changeOwnerPermsTrasnactionId2)))).get + s = i.executeAction(s, LocalAction(readFileInvocId, Return())).get + println("read") + + + println(s"done"); + + try { + i.checkInvariants(s) + } catch { + case iv: InvariantViolationException => + fail("Invariant-check should pass") + println(iv) + for (info <- iv.info) + println(info) + } + + } + + test("file_system_pass2") { + + val prog = Repliss.parseAndTypecheck("fs", Helper.getResource("/examples/buggy/5.rpls")).get() + val i = new Interpreter(prog, RunArgs(), domainSize = 3) + var s = Interpreter.State() + + val createAdminInvocId = InvocationId(1); + val createUserInvocId = InvocationId(2); + val createGroupInvocId = InvocationId(3); + val assignToGroupInvocId = InvocationId(4); + val createFileInvocId = InvocationId(5); + val changeOwnerPermsInvocId = InvocationId(6); + val readFileInvocId = InvocationId(7); + + + val createAdminTrasnactionId = TransactionId(1); + val createUserTrasnactionId = TransactionId(2); + val createGroupTransactionId = TransactionId(3); + val assignToGroupTransactionId = TransactionId(4); + val createFileTrasnactionId = TransactionId(5); + val changeOwnerPermsTrasnactionId = TransactionId(6); + val readFileTrasnactionId = TransactionId(7); + + + val admin1 = domainValue("UserId", 1); + val user1 = domainValue("UserId", 2); + val file1 = domainValue("NodeId", 1); + val group1 = domainValue("GroupId", 1); + val writAccessRight = AnyValue(DataTypeValue("AW", List())); + + // create admin + s = i.executeAction(s, CallAction(createAdminInvocId, "createUser", List(AnyValue(true)))).get // create admin + s = i.executeAction(s, LocalAction(createAdminInvocId, StartTransaction(createAdminTrasnactionId, Set()))).get + s = i.executeAction(s, LocalAction(createAdminInvocId, NewId(1))).get + s = i.executeAction(s, LocalAction(createAdminInvocId, Return())).get + println(s"admin created"); + + // create user + s = i.executeAction(s, CallAction(createUserInvocId, "createUser", List(AnyValue(false)))).get // create admin + s = i.executeAction(s, LocalAction(createUserInvocId, StartTransaction(createUserTrasnactionId, Set()))).get + s = i.executeAction(s, LocalAction(createUserInvocId, NewId(2))).get + s = i.executeAction(s, LocalAction(createUserInvocId, Return())).get + println(s"user created"); + + // create group + s = i.executeAction(s, CallAction(createGroupInvocId, "createGroup", List())).get // create admin + s = i.executeAction(s, LocalAction(createGroupInvocId, StartTransaction(createGroupTransactionId, Set()))).get + s = i.executeAction(s, LocalAction(createGroupInvocId, NewId(1))).get + s = i.executeAction(s, LocalAction(createGroupInvocId, Return())).get + println("Group created") + + // assign user to group + s = i.executeAction(s, CallAction(assignToGroupInvocId, "assignUserToGroup", List(admin1, group1, user1))).get + s = i.executeAction(s, LocalAction(assignToGroupInvocId, StartTransaction(assignToGroupTransactionId, Set(createUserTrasnactionId, createAdminTrasnactionId)))).get + s = i.executeAction(s, LocalAction(assignToGroupInvocId, Return())).get + println(s"user assigned to group"); + + // create file + s = i.executeAction(s, CallAction(createFileInvocId, "createFile", List(user1, group1))).get + s = i.executeAction(s, LocalAction(createFileInvocId, StartTransaction(createFileTrasnactionId, Set(assignToGroupTransactionId)))).get + s = i.executeAction(s, LocalAction(createFileInvocId, NewId(1))).get + s = i.executeAction(s, LocalAction(createFileInvocId, Return())).get + println(s"file created"); + + // change owner perms + s = i.executeAction(s, CallAction(changeOwnerPermsInvocId, "changeOwnerPermission", List(admin1, writAccessRight, file1))).get + s = i.executeAction(s, LocalAction(changeOwnerPermsInvocId, StartTransaction(changeOwnerPermsTrasnactionId, Set(createFileTrasnactionId)))).get + s = i.executeAction(s, LocalAction(changeOwnerPermsInvocId, Return())).get + println(s"owner perms changed"); + + // read + s = i.executeAction(s, CallAction(readFileInvocId, "readFile", List(user1, file1))).get + s = i.executeAction(s, LocalAction(readFileInvocId, StartTransaction(readFileTrasnactionId, Set(changeOwnerPermsTrasnactionId)))).get + s = i.executeAction(s, LocalAction(readFileInvocId, Return())).get + println(s"done"); + + try { + i.checkInvariants(s) + } catch { + case iv: InvariantViolationException => + fail("Invariant-check should fail") + println(iv) + for (info <- iv.info) + println(info) + } + + } + } From d5efd92f006d7a04c3092c82485bee8a6848ffc1 Mon Sep 17 00:00:00 2001 From: Michael Youssef Date: Tue, 2 Feb 2021 18:40:29 +0100 Subject: [PATCH 10/10] implement upper bound --- .../crdts/AFileAccessRightsCrdt.scala | 38 ++++++++++--------- 1 file changed, 20 insertions(+), 18 deletions(-) diff --git a/jvm/src/main/scala/crdtver/language/crdts/AFileAccessRightsCrdt.scala b/jvm/src/main/scala/crdtver/language/crdts/AFileAccessRightsCrdt.scala index ce2552a..42e403b 100644 --- a/jvm/src/main/scala/crdtver/language/crdts/AFileAccessRightsCrdt.scala +++ b/jvm/src/main/scala/crdtver/language/crdts/AFileAccessRightsCrdt.scala @@ -148,40 +148,42 @@ class AFileAccessRightsCrdt extends CrdtTypeDefinition { override def additionalDataTypesRec: List[TypedAst.InTypeDecl] = AFileAccessRightsCrdt.this.additionalDataTypes - // TODO: def _upperBoundedByOrEq(val1: InExpr, val2: InExpr): InExpr = ( ( - val1 === mkDatatypeCase("None", T) && - (val2 === mkDatatypeCase("None", T) || val2 === mkDatatypeCase("R", T) || val2 === mkDatatypeCase("W", T) || val2 === mkDatatypeCase("X", T) - || val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + val1 === mkDatatypeCase("ANone", T) && + (val2 === mkDatatypeCase("ANone", T) || val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) || val2 === mkDatatypeCase("ARW", T)) ) || ( - val1 === mkDatatypeCase("R", T) && - (val2 === mkDatatypeCase("R", T) || val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("RWX", T)) + val1 === mkDatatypeCase("AR", T) && + (val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("ARW", T)) ) || ( - val1 === mkDatatypeCase("W", T) && - (val2 === mkDatatypeCase("W", T) || val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + val1 === mkDatatypeCase("AW", T) && + (val2 === mkDatatypeCase("AW", T) || val2 === mkDatatypeCase("ARW", T)) ) || ( - val1 === mkDatatypeCase("X", T) && - (val2 === mkDatatypeCase("X", T) || val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + val1 === mkDatatypeCase("ARW", T) && + val2 === mkDatatypeCase("ARW", T) ) || ( - val1 === mkDatatypeCase("RW", T) && - (val2 === mkDatatypeCase("RW", T) || val2 === mkDatatypeCase("RWX", T)) + val1 === mkDatatypeCase("UNone", T) && + ( val2 === mkDatatypeCase("URW", T) || val2 === mkDatatypeCase("UR", T) || val2 === mkDatatypeCase("UW", T) || val2 === mkDatatypeCase("UNone", T) + || val2 === mkDatatypeCase("ARW", T) || val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T)) ) || ( - val1 === mkDatatypeCase("RX", T) && - (val2 === mkDatatypeCase("RX", T) || val2 === mkDatatypeCase("RWX", T)) + val1 === mkDatatypeCase("UR", T) && + ( val2 === mkDatatypeCase("UR", T) || val2 === mkDatatypeCase("URW", T) || val2 === mkDatatypeCase("ARW", T) + || val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T)) ) || ( - val1 === mkDatatypeCase("WX", T) && - (val2 === mkDatatypeCase("WX", T) || val2 === mkDatatypeCase("RWX", T)) + val1 === mkDatatypeCase("UW", T) && + ( val2 === mkDatatypeCase("UW", T) || val2 === mkDatatypeCase("URW", T) || val2 === mkDatatypeCase("ARW", T) + || val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T)) ) || ( - val1 === mkDatatypeCase("RWX", T) && - val2 === mkDatatypeCase("RWX", T) + val1 === mkDatatypeCase("URW", T) && + ( val2 === mkDatatypeCase("URW", T) || val2 === mkDatatypeCase("ARW", T) + || val2 === mkDatatypeCase("AR", T) || val2 === mkDatatypeCase("AW", T) ||val2 === mkDatatypeCase("ANone", T)) ) )