recursive operator issue

[timimin]

Recursion issue

Hi. I'm working on a TLA+/TLC project. The project is complex enough. So I'm trying to achieve productivity gains when checking invariant safety property of the system and now trying to transform specifications to the format eligible for Apalache. It is worth to say that specifications include a number of recursive operators. I've successfully passed the typing phase but stumble over rather subtle exceptions.
To replay them I've created a simple spec

VARIABLES 

\* @type: Set(Set(Str));
set1,

\* @type: Set(Str);
set2

\* @type: <<Set(Set(Str)), Set(Str)>>;
vars == <<set1, set2>>

RECURSIVE FoldSet(_,_,_)
FoldSet( Op(_,_), v, S ) == IF S = {}
                            THEN v
                            ELSE LET w == CHOOSE x \in S: TRUE
                                  IN LET T == S \ {w}
                                      IN FoldSet( Op, Op(v,w), T )

\* @type: (Set(a), Set(a)) =>  Set(a);      
UnionSet_OP(x, y) == x \cup y
UnionSet(set) == FoldSet(UnionSet_OP, {}, set)   

UNROLL_DEFAULT_FoldSet == 0
UNROLL_TIMES_FoldSet == 2

Init ==
        /\ set1 = {{"x","y"}, {"a","b"}}
        /\ set2 = {}
        
Next == 
        \/ /\ set1 # {}
           /\ set2' = UnionSet(set1)
           /\ set1' = {}            
        \/ /\ set1 = {}
           /\ UNCHANGED vars
        
Inv == /\ "x" \notin set2

SpecFS == Init /\ [] [Next]_vars 

which works normally in TLC.
But Apalache generates the following:

...
PASS #11: AnalysisPass                                            I@13:39:36.986
 > Marking skolemizable existentials and sets to be expanded...   I@13:39:36.988
  > SkolemizationMarker                                           I@13:39:36.989
  > ExpansionMarker                                               I@13:39:36.990
 > Running analyzers...                                           I@13:39:36.995
  > Introduced expression grades                                  I@13:39:37.009
  > Introduced 4 formula hints                                    I@13:39:37.009
PASS #12: PostTypeCheckerSnowcat                                  I@13:39:37.009
 > Running Snowcat .::.                                           I@13:39:37.010
[Paralocks.tla:18:38-19:66]: No match between operator signature ((Set(Str)) => Set(Str)) and argument Int E@13:39:37.096
[unknown location]: Error when computing the type of Next$0       E@13:39:37.097
 > Snowcat asks you to fix the types. Meow.                       I@13:39:37.098

Additionally i would like to ask, why does it require to annotate FoldSet with UNROLL_DEFAULT_FoldSet and UNROLL_TIMES_FoldSet. Accordingly to the guide this very operator can be used without these restrictive annotations (. It is obvious that in real life we often use algorithmic constructions to operate on sets and sequences and in most cases we cannot assign an upper bound on the number of iterations inside recursive operators. Thankfully in most cases we can handle datasets using FoldSet and FoldSequence operators only. If the upper bound of iterations can not be derived automatically then should we choose an obviously larger value?

Sometimes recursion appears in community tla+ modules i.e FinitSets...

Thanks in advance. Alex.

[Kukovec]

Hi @timimin!

A couple of things:

• Primarily, the problem is, that you're trying to define your own FoldSet operator, instead of using the one defined in the Apalache module. All you need to do is add EXTENDS Apalache and use it in the same way you use FoldSet now (it does not need UNROLL_... operators). See https://apalache.informal.systems/docs/apalache/fold.html for more details on the FoldSet defined in Apalache.
• The reason why UNROLL_DEFAULT_ and UNROLL_TIMES_ must be given, when defining recursive operators, is that Apalache does not dynamically evaluate expressions like TLC does, but instead represents them as symbolic constraints passed to an SMT solver. In the case of recursive operators, the problem is the inability to statically determine the amount of recursive steps evaluating an expression would take. It could be 0 or it could be infinitely many, since it's easy to write non-terminating recursion. The compromise in Apalache is that recursive operators get unrolled UNROLL_TIMES_X-number of times, with the UNROLL_TIMES_X + 1th unroll value replaced by UNROLL_DEFAULT_X (see https://apalache.informal.systems/docs/apalache/principles.html?#recursive-operators and https://apalache.informal.systems/docs/apalache/fold.html?#folding-vs-recursion).

We have found that, in practice, using the folds defined by the Apalache module, recursive operators are almost always unnecessary, and it's very likely that we will end up restricting their use in the future.

As an aside, the reason you're getting errors in your specification is UNROLL_DEFAULT_FoldSet == 0, which locks the return type of your implementation of FoldSet to Int. However, you call UnionSet(set1), where Init defines set1= {{"x","y"}, {"a","b"}}, which would require a fold operator with a return type of Set(Str), thus the error ... No match between operator signature ((Set(Str)) => Set(Str)) and argument Int. Since TLC ignores UNROLL_DEFAULT_, this doesn't end up causing an error there.

[timimin]

Oh... Thanks a lot. Everything is clear now. I didn't figure out the meaning of UNROL­L_DEFAULT_ , so i took the default int value as in the example... (thought it might be the minimum times the operator can unfold )... Thanks -- Отправлено из Mail.ru для Android воскресенье, 14 ноября 2021г., 23:10 +03:00 от Kukovec ***@***.*** :

…

Hi @timimin ! A couple of things: * Primarily, the problem is, that you're trying to define your own FoldSet operator, instead of using the one defined in the Apalache module. All you need to do is add EXTENDS Apalache and use it in the same way you use FoldSet now. See https://apalache.informal.systems/docs/apalache/fold.html for more details on the FoldSet defined in Apalache. * The reason why UNROLL_DEFAULT_ and UNROLL_TIMES_ must be given, when defining recursive operators, is that Apalache does not dynamically evaluate expressions like TLC does, but instead represents them as symbolic constraints passed to an SMT solver. In the case of recursive operators, the problem is the inability to statically determine the amount of recursive steps evaluating an expression would take. It could be 0 or it could be infinitely many, since it's easy to write non-terminating recursion. The compromise in Apalache is that recursive operators get unrolled UNROLL_TIMES_X-number of times, with the UNROLL_TIMES_X + 1th unroll value replaced by UNROLL_DEFAULT_X (see https://apalache.informal.systems/docs/apalache/principles.html?#recursive-operators and https://apalache.informal.systems/docs/apalache/fold.html?#folding-vs-recursion ). We have found that, in practice, using the folds defined by the Apalache module, recursive operators are almost always unnecessary, and it's very likely that we will end up restricting their use in the future. As an aside, the reason you're getting errors in your specification is UNROLL_DEFAULT_FoldSet == 0, which locks the return type of your implementation of FoldSet to Int. However, you call UnionSet(set1), where Init defines set1= {{"x","y"}, {"a","b"}}, which would require a fold operator with a return type of Set(Str), thus the error ... No match between operator signature ((Set(Str)) => Set(Str)) and argument Int. Since TLC ignores UNROLL_DEFAULT_, this doesn't end up causing an error there. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub , or unsubscribe . Triage notifications on the go with GitHub Mobile for iOS or Android .