diff --git a/docs/src/lang/apalache-operators.md b/docs/src/lang/apalache-operators.md index 50e2b00fe4..419cf3baff 100644 --- a/docs/src/lang/apalache-operators.md +++ b/docs/src/lang/apalache-operators.md @@ -175,49 +175,59 @@ MkSeq(3, Double) = <<2, 4, 6>> \* TRUE ## Interpret a function as a sequence -**Notation:** `FunAsSeq(fn, maxLen)` +**Notation:** `FunAsSeq(fn, len, maxLen)` -**LaTeX notation:** `FunAsSeq(fn, maxLen)` +**LaTeX notation:** `FunAsSeq(fn, len, maxLen)` -**Arguments:** Two arguments. The first is a function, the second is an integer. +**Arguments:** Three arguments: -**Apalache type:** `(Int -> a, Int) => Seq(a)`, for some type `a` +* A function `fn` that should be interpreted as a sequence. +* An integer `len`, denoting the length of the sequence, with the property + `1..len \subseteq DOMAIN fn`. Apalache does not check this requirement. It is up to the user to ensure that it holds. This expression is not necessarily constant. +* An integer constant `maxLen`, which is an upper bound on `len`, that is, `len <= maxLen`. -**Effect:** The expression `FunAsSeq(fn, maxLen)` evaluates to the sequence `<< fn[1], ..., fn[maxLen] >>`. -At the level of Apalache static analysis, `FunAsSeq` indicates type-casting a function type `Int -> a` to a sequence type `Seq(a)`, since one cannot use function constructors to define a sequence in Apalache otherwise. +**Apalache type:** `(Int -> a, Int, Int) => Seq(a)`, for some type `a` + +**Effect:** The expression `FunAsSeq(fn, len, maxLen)` evaluates to the +sequence `<< fn[1], ..., fn[Min(len, maxLen)] >>`. **Determinism:** Deterministic. -**Errors:** -If `fn` is not a function of the type `Int -> a` or if `maxLen` is not an integer, Apalache statically reports a type error. Additionally, if it is not the case that `1..maxLen \subseteq DOMAIN fn`, the result is undefined. +**Errors:** If the types of `fn`, `len` or `maxLen` do not match the expected types, Apalache statically reports a +type error. Additionally, if it is not the case that `1..len \subseteq DOMAIN fn`, the result is undefined. **Example in TLA+:** ```tla -Head( [ x \in 1..5 |-> x * x ] ) \* 1 in TLC, type error in Apalache -FunAsSeq( [ x \in 1..5 |-> x * x ], 3 ) \* <<1,4,9>> -Head( FunAsSeq( [ x \in 1..5 |-> x * x ], 3 ) ) \* 1 -FunAsSeq( <<1,2,3>>, 3 ) \* <<1,2,3>> in TLC, type error in Apalache -FunAsSeq( [ x \in {0,42} |-> x * x ], 3 ) \* UNDEFINED +Head([ x \in 1..5 |-> x * x ]) \* 1 in TLC, type error in Apalache +FunAsSeq([ x \in 1..5 |-> x * x ], 3, 3) \* <<1,4,9>> +Head(FunAsSeq([ x \in 1..5 |-> x * x ], 3, 3)) \* 1 +FunAsSeq(<<1,2,3>>, 3, 3) \* <<1,2,3>> in TLC, type error in Apalache +FunAsSeq([ x \in {0,42} |-> x * x ], 3, 3) \* UNDEFINED ``` **Example in Python:** ```python -def funAsSeq(f,imax): - # f === { x:f(x) | x \in Dom(f) } - return[f.get(i) for i in range(1,imax+1)] +# define a TLA+-like dictionary via a python function def boundedFn(f, dom): - return { x:f(x) for x in dom } -f = boundedFn( lambda x: x*x, range(1,6) ) # [ x \in 1..5 |-> x * x ] -g = boundedFn( lambda x: x*x, {0,42} ) # [ x \in {0,42} |-> x * x ] ->>> f[1] # Head( [ x \in 1..5 |-> x * x ] ) + return { x: f(x) for x in dom } + +# this is how we could define funAsSeq in python +def funAsSeq(f, length, maxLen): + return [ f.get(i) for i in range(1, min(length, maxLen) + 1) ] + +# TLA+: [ x \in 1..5 |-> x * x ] +f = boundedFn(lambda x: x * x, range(1,6)) +# TLA+: [ x \in {0, 42} |-> x * x ] +g = boundedFn(lambda x: x * x, {0, 42}) +>>> f[1] 1 ->>> funAsSeq(f, 3) # FunAsSeq( [ x \in 1..5 |-> x * x ], 3 ) -[1,4,9] ->>> funAsSeq(f, 3)[1] # Head( FunAsSeq( [ x \in 1..5 |-> x * x ], 3 ) ) +>>> funAsSeq(f, 3, 3) +[1, 4, 9] +>>> funAsSeq(f, 3, 3)[1] 1 ->>> funAsSeq( g, 3 ) # FunAsSeq( [ x \in {0,42} |-> x * x ], 3 ) +>>> funAsSeq(g, 3, 3) [None, None, None] ``` diff --git a/src/tla/Apalache.tla b/src/tla/Apalache.tla index 0384fd20a5..5ddfcb4afa 100644 --- a/src/tla/Apalache.tla +++ b/src/tla/Apalache.tla @@ -66,16 +66,26 @@ MkSeq(N, F(_)) == \* This is the TLC implementation. Apalache does it differently. [ i \in (1..N) |-> F(i) ] +\* required by our default definition of FoldSeq and FunAsSeq +LOCAL INSTANCE Sequences + (** * As TLA+ is untyped, one can use function- and sequence-specific operators * interchangeably. However, to maintain correctness w.r.t. our type-system, * an explicit cast is needed when using functions as sequences. * - * @type: ((Int -> a), Int) => Seq(a); + * The parameters have the following meaning: + * + * - fn is the function from 1..len that should be interpreted as a sequence. + * - len is the length of the sequence, len = Cardinality(DOMAIN fn), + * len may be a variable, a computable expression, etc. + * - capacity is a static upper bound on the length, that is, len <= capacity. + * + * @type: ((Int -> a), Int, Int) => Seq(a); *) -FunAsSeq(fn, maxSeqLen) == +FunAsSeq(fn, len, capacity) == LET __FunAsSeq_elem_ctor(i) == fn[i] IN - MkSeq(maxSeqLen, __FunAsSeq_elem_ctor) + SubSeq(MkSeq(capacity, __FunAsSeq_elem_ctor), 1, len) (** * Annotating an expression \E x \in S: P as Skolemizable. That is, it can @@ -112,9 +122,6 @@ FoldSet( Op(_,_), v, S ) == IF S = {} IN LET T == S \ {w} IN FoldSet( Op, Op(v,w), T ) -\* required by our default definition of FoldSeq -LOCAL INSTANCE Sequences - (** * The folding operator, used to implement computation over a sequence. * Apalache implements a more efficient encoding than the one below. diff --git a/test/tla/MC_QueensTyped.tla b/test/tla/MC_QueensTyped.tla new file mode 100644 index 0000000000..7b4b83b8fe --- /dev/null +++ b/test/tla/MC_QueensTyped.tla @@ -0,0 +1,12 @@ +---------------------------- MODULE MC_QueensTyped ---------------------------- +\* an instance of QueensTyped for model checking. +N == 4 + +VARIABLES + \* @type: Set(Seq(Int)); + todo, + \* @type: Set(Seq(Int)); + sols + +INSTANCE QueensTyped +=============================================================================== diff --git a/test/tla/MegaSpec1.tla b/test/tla/MegaSpec1.tla index 4d84aff491..cf57857366 100644 --- a/test/tla/MegaSpec1.tla +++ b/test/tla/MegaSpec1.tla @@ -147,5 +147,5 @@ RealDiv(x, y) == x / y \* Apalache \* @type: (Int -> Str) => Seq(Str); -Fas(f) == FunAsSeq(f, 3) -=============================================================================== \ No newline at end of file +Fas(f) == FunAsSeq(f, 3, 3) +=============================================================================== diff --git a/test/tla/QueensTyped.tla b/test/tla/QueensTyped.tla index 3380c37a18..9dd4b0ba92 100644 --- a/test/tla/QueensTyped.tla +++ b/test/tla/QueensTyped.tla @@ -44,10 +44,10 @@ IsSolution(queens) == \* We apply Apalache!FunAsSeq to convert a function to a sequence. Solutions == LET Queens == { queens \in [1..N -> 1..N] : - IsSolution(FunAsSeq(queens, N)) } IN + IsSolution(FunAsSeq(queens, N, N)) } IN \* We have to apply FunAsSeq twice, as queens is used as a sequence twice. \* A better approach would be to refactor the spec, to call FunAsSeq once. - { FunAsSeq(queens, N): queens \in Queens } + { FunAsSeq(queens, N, N): queens \in Queens } (***************************************************************************) (* We now describe an algorithm that iteratively computes the set of *) diff --git a/test/tla/TestSequences.tla b/test/tla/TestSequences.tla index f3b8e1f4d0..76507259f5 100644 --- a/test/tla/TestSequences.tla +++ b/test/tla/TestSequences.tla @@ -178,14 +178,19 @@ TestFoldSeqOverSelectSeq == TestFunAsSeq3 == LET f == [ i \in 1..3 |-> i + 1 ] IN - FunAsSeq(f, 3) = <<2, 3, 4>> + FunAsSeq(f, 3, 3) = <<2, 3, 4>> TestFunAsSeqEmpty == LET \* @type: Int -> Int; f == [ i \in {} |-> i ] IN - FunAsSeq(f, 0) = << >> + FunAsSeq(f, 0, 0) = << >> + +TestFunAsSeqLargerCapacity == + LET f == [ i \in 1..3 |-> i + 1 ] IN + \* provide a larger upper bound + FunAsSeq(f, 3, 10) = <<2, 3, 4>> TestExceptLen == Len([seq345 EXCEPT ![2] = 10]) = 3 @@ -235,6 +240,7 @@ AllTests == /\ TestMkSeqFold /\ TestFunAsSeq3 /\ TestFunAsSeqEmpty + /\ TestFunAsSeqLargerCapacity /\ TestExceptLen /\ TestExceptDomain =============================================================================== diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/MkSeqRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/MkSeqRule.scala index bbd9434de5..212f33fd74 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/MkSeqRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/MkSeqRule.scala @@ -10,7 +10,7 @@ import at.forsyte.apalache.tla.lir.oper.ApalacheOper import at.forsyte.apalache.tla.lir.storage.BodyMapFactory import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker import at.forsyte.apalache.tla.lir.values.TlaInt -import at.forsyte.apalache.tla.pp.{ConstSimplifier, InlinerOfUserOper, TlaInputError} +import at.forsyte.apalache.tla.pp.{InlinerOfUserOper, TlaInputError} /** * Rewriting rule for MkSeq. This rule is similar to [[FoldSeqRule]]. @@ -20,7 +20,6 @@ import at.forsyte.apalache.tla.pp.{ConstSimplifier, InlinerOfUserOper, TlaInputE */ class MkSeqRule(rewriter: SymbStateRewriter) extends RewritingRule { private val proto = new ProtoSeqOps(rewriter) - private val simplifier = new ConstSimplifier(new IdleTracker()) override def isApplicable(symbState: SymbState): Boolean = symbState.ex match { // match the internal representation of lambda expressions or embedded calls @@ -71,7 +70,7 @@ class MkSeqRule(rewriter: SymbStateRewriter) extends RewritingRule { // extract capacity from the length expression private def extractCapacity(lenEx: TlaEx): Int = { - simplifier(lenEx) match { + lenEx match { case ValEx(TlaInt(n)) if n.isValidInt && n >= 0 => n.toInt diff --git a/tla-types/src/test/resources/MegaSpec1.tla b/tla-types/src/test/resources/MegaSpec1.tla index ef3c873047..17f47d4de1 100644 --- a/tla-types/src/test/resources/MegaSpec1.tla +++ b/tla-types/src/test/resources/MegaSpec1.tla @@ -162,5 +162,5 @@ RealDiv(x, y) == x / y \* Apalache \* @type: (Int -> Str) => Seq(Str); -Fas(f) == FunAsSeq(f, 3) +Fas(f) == FunAsSeq(f, 3, 3) =============================================================================== \ No newline at end of file