Open craft095 opened 2 years ago
shonfeder
commented
2 years ago Thanks for the bug report, @craft095! To help us prioritize, could you let us know whether this bug is currently blocking your ability to use Apalache for checking your specs, or are you able to use a workarounds?
shonfeder
commented
2 years ago IIUC, the key problem here is just that we aren't normalizing the types before running our equality check. We are trying to compare values which of these two types:
FinFunSet[CellTFrom(Set(Bool)), CellTFrom(Set(Bool))] CellTFrom(Set((Bool -> Bool))) which should be equivalent, afaict.
But we don't have a case for this combination in
so we are falling back to the default error case.
Rather than add special cases to handle these permutations, I think we should ensure the types are normalized to a canonical form before we make these kinds of checks.
konnov
commented
2 years ago This is a missing feature. I would say that is blocked by #1452. Internally, FinFunSet corresponds to a function set that is defined via [ S -> T ]. If we want to compare it to an explicitly constructed set such as { x \in S: CHOOSE y \in T: TRUE }, we would have to expand the set [ S -> T ].
This issue goes to the box of https://github.com/informalsystems/apalache/milestone/56, which requires some systematic refactoring. We plan to do this in Q4.
craft095
commented
2 years ago I see, thank you. Could you help me with workaround? I managed to construct [D -> R] explicitly, but I cannot get types right to make Apalache happy:
---- MODULE Apalache_M0 ----
EXTENDS Naturals, FiniteSets
\* @type: (Set(a), Set(b)) => Set(a -> b);
FSets(D, R) ==
LET
\* @type: Int -> Set(a -> b);
F[n \in 0..Cardinality(D)] ==
IF n = 0
THEN {<<>>}
ELSE
LET
\* @type: Set(a -> b);
F0 == F[n - 1]
\* All functions in F0 have the same domain, choose any one
\* @type: a -> b;
f0 == CHOOSE f \in F0 : TRUE
\* @type: Set(a);
D_smaller == DOMAIN f0
\* @type: a;
d1 == CHOOSE d \in (D \ D_smaller) : TRUE
\* @type: Set(a);
D_bigger == D_smaller \union {d1}
IN
{
[d \in D_bigger |-> IF d \in DOMAIN f THEN f[d] ELSE r]
: f \in F0, r \in R
}
IN
F[Cardinality(D)]
ASSUME
\A d \in SUBSET (0..3) :
\A r \in SUBSET (4..5) :
[d -> r] = FSets(d, r)
====Log:
# APALACHE version: 0.25.7 | build: 554bdb5 I@12:24:51.712
Checker options: check --out-dir=C:\work\TLA\tlc-qual\.tmp --run-dir=C:\work\TLA\tlc-qual\.tmp --length=5 C:\work\TLA\tlc-qual\draft.sandbox\Let\FunSet\dl\ref\Apalache_M0.tla I@12:24:51.887
Tuning: I@12:24:51.887
PASS #0: SanyParser I@12:24:51.887
Parsing file C:\work\TLA\tlc-qual\draft.sandbox\Let\FunSet\dl\ref\Apalache_M0.tla
Parsing file C:\Users\dkulagin\AppData\Local\Temp\Naturals.tla
Parsing file C:\Users\dkulagin\AppData\Local\Temp\FiniteSets.tla
Parsing file C:\Users\dkulagin\AppData\Local\Temp\__rewire_sequences_in_apalache.tla
Parsing file C:\Users\dkulagin\AppData\Local\Temp\__apalache_folds.tla
PASS #1: TypeCheckerSnowcat I@12:24:52.193
> Running Snowcat .::. I@12:24:52.193
[Apalache_M0.tla:20:34-20:42]: Annotation required. Found 4 matching operator signatures (((a40 -> a41)) => Set(a40)) or ((Seq(a42)) => Set(Int)) or (([]) => Set(Str)) or ((<| |>) => Set(Int)) for argument a102 E@12:24:52.415
[Apalache_M0.tla:20:21-20:42]: Error when computing the type of D_smaller E@12:24:52.426
> Snowcat asks you to fix the types. Meow. I@12:24:52.426
Checker has found an error I@12:24:52.426
It took me 0 days 0 hours 0 min 0 sec I@12:24:52.426
Total time: 0.712 sec I@12:24:52.426
EXITCODE: ERROR (120)Hi @craft095!
I am trying to reproduce your example. There are several things:
IF-THEN-ELSE, see #1962. This is probably caused by some irregularity in the SANY parser. This needs some investigation.So for (1), you have an easy workaround. For (2), I am not sure about what's happening. However, even if you fix it, we have dropped support for recursive operators and functions in favor of folds: https://apalache.informal.systems/docs/apalache/principles/recursive.html
craft095
commented
2 years ago @konnov , thank you for hint! I managed to do it with fold:
\* @type: (Set(a), Set(b)) => Set(a -> b);
FSets(D, R) ==
LET
\* Empty function
fe == [x \in D \ D |-> CHOOSE r \in R : TRUE]
\* @type: (Set(a -> b), a) => Set(a -> b);
F(F0, d1) ==
LET
\* All functions in F0 have the same domain, choose any one
\* @type: a -> b;
f0 == CHOOSE f \in F0 : TRUE
\* @type: Set(a);
D_smaller == DOMAIN f0
\* @type: Set(a);
D_bigger == D_smaller \union {d1}
IN
{
[d \in D_bigger |-> IF d /= d1 THEN f[d] ELSE r]
: f \in F0, r \in R
}
IN
ApaFoldSet(F, {fe}, D)
Description
Comparison of two sets of functions, one of which is of form
[X -> Y]leads toUnexpected equality testerrorInput specification
The command line parameters used to run the tool
Expected behavior
No error is expected
Log files
System information
0.25.7 build 554bdb5:Windows 10:18.0.1: