search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
441 stars 40 forks source link

Rewriter error: Range bounds are too large to fit in scala.Int #2151

Open andrey-kuprianov opened 2 years ago

andrey-kuprianov commented 2 years ago

Impact

This seems to be a bug, as it tries to fit unbounded integers in the spec into bounded integers in Scala.

PASS #13: BoundedChecker                                          I@18:24:00.914
test.tla:15:62-15:77: rewriter error: Range bounds are too large to fit in scala.Int E@18:24:02.741
at.forsyte.apalache.infra.AdaptedException: test.tla:15:62-15:77: rewriter error: Range bounds are too large to fit in scala.Int
        at at.forsyte.apalache.infra.Executor.run(Executor.scala:37)
        at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:87)
        at at.forsyte.apalache.tla.Tool$.runCommand(Tool.scala:135)
        at at.forsyte.apalache.tla.Tool$.run(Tool.scala:115)
        at at.forsyte.apalache.tla.Tool$.main(Tool.scala:36)
        at at.forsyte.apalache.tla.Tool.main(Tool.scala)

Besides that, what I want to achieve, is to express a non-deterministic choice of action. It should be possible to do simpler than in the example; I would be grateful for help on how to express the desired behavior by possibly other means.

Input specification

---- MODULE test ----
EXTENDS Apalache, Integers

VARIABLES
    \* @typeAlias: COIN = [denom: Str, amount: Int];
    \* @typeAlias: ACTION = [sender: Str, receiver: Str, coins: Set(COIN)];
    \* @type: ACTION;
    action

WALLETS == {"Alice", "Bob", "Carol", "Dave", "Eve"}
MAX_BALANCE == 2^256-1

DENOMS == {"a", "b", "c"}

COINS == { [denom |-> d, amount |-> a] : d \in DENOMS, a \in 0 .. MAX_BALANCE }

\* @type: (ACTION) => Bool;
NewAction(a) ==
  a \in [ sender: WALLETS, receiver: WALLETS, coins: SUBSET COINS ]

Init == NewAction(action)

Next == NewAction(action')

=====

The command line parameters used to run the tool

apalache check test.tla

Expected behavior

Log files

``` 2022-09-06T18:23:59,131 [main] INFO a.f.a.t.Tool\$ - # APALACHE version: 0.28.0 | build: 3d945af 2022-09-06T18:23:59,134 [main] INFO a.f.a.t.t.o.CheckCmd - Tuning: search.outputTraces=false 2022-09-06T18:23:59,136 [main] INFO a.f.a.t.t.o.CheckCmd - Checker options: check test.tla 2022-09-06T18:23:59,141 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser 2022-09-06T18:23:59,863 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK] 2022-09-06T18:23:59,864 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat 2022-09-06T18:23:59,864 [main] INFO a.f.a.t.t.p.EtcTypeCheckerPassImpl - > Running Snowcat .::. 2022-09-06T18:23:59,963 [main] WARN a.f.a.t.t.TypeCheckerTool - Operator action: Deprecated syntax in type alias COIN. Use camelCase of Type System 1.2. 2022-09-06T18:24:00,149 [main] WARN a.f.a.t.t.TypeCheckerTool - Operator action: Deprecated syntax in type alias ACTION. Use camelCase of Type System 1.2. 2022-09-06T18:24:00,617 [main] INFO a.f.a.t.t.p.EtcTypeCheckerPassImpl - > Your types are purrfect! 2022-09-06T18:24:00,617 [main] INFO a.f.a.t.t.p.EtcTypeCheckerPassImpl - > All expressions are typed 2022-09-06T18:24:00,621 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat [OK] 2022-09-06T18:24:00,622 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass 2022-09-06T18:24:00,634 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Command line option --init is not set. Using Init 2022-09-06T18:24:00,635 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Command line option --next is not set. Using Next 2022-09-06T18:24:00,635 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set the initialization predicate to Init 2022-09-06T18:24:00,636 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set the transition predicate to Next 2022-09-06T18:24:00,643 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass [OK] 2022-09-06T18:24:00,644 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass 2022-09-06T18:24:00,645 [main] INFO a.f.a.t.p.p.DesugarerPassImpl - > Desugaring... 2022-09-06T18:24:00,654 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass [OK] 2022-09-06T18:24:00,655 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass 2022-09-06T18:24:00,656 [main] INFO a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next 2022-09-06T18:24:00,706 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass [OK] 2022-09-06T18:24:00,707 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #5: TemporalPass 2022-09-06T18:24:00,708 [main] INFO a.f.a.t.p.p.TemporalPassImpl - > Rewriting temporal operators... 2022-09-06T18:24:00,708 [main] INFO a.f.a.t.p.p.TemporalPassImpl - > No temporal property specified, nothing to encode 2022-09-06T18:24:00,709 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #5: TemporalPass [OK] 2022-09-06T18:24:00,710 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #6: InlinePass 2022-09-06T18:24:00,711 [main] INFO a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next 2022-09-06T18:24:00,716 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #6: InlinePass [OK] 2022-09-06T18:24:00,719 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #7: PrimingPass 2022-09-06T18:24:00,721 [main] INFO a.f.a.t.a.p.PrimingPassImpl - > Introducing InitPrimed for Init' 2022-09-06T18:24:00,724 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #7: PrimingPass [OK] 2022-09-06T18:24:00,724 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #8: VCGen 2022-09-06T18:24:00,724 [main] INFO a.f.a.t.b.p.VCGenPassImpl - > No invariant given. Only deadlocks will be checked 2022-09-06T18:24:00,726 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #8: VCGen [OK] 2022-09-06T18:24:00,726 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #9: PreprocessingPass 2022-09-06T18:24:00,726 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Before preprocessing: unique renaming 2022-09-06T18:24:00,732 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Applying standard transformations: 2022-09-06T18:24:00,733 [main] INFO a.f.a.t.p.p.PreproPassImpl - > PrimePropagation 2022-09-06T18:24:00,734 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Desugarer 2022-09-06T18:24:00,739 [main] INFO a.f.a.t.p.p.PreproPassImpl - > UniqueRenamer 2022-09-06T18:24:00,743 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Normalizer 2022-09-06T18:24:00,745 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Keramelizer 2022-09-06T18:24:00,757 [main] INFO a.f.a.t.p.p.PreproPassImpl - > After preprocessing: UniqueRenamer 2022-09-06T18:24:00,767 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #9: PreprocessingPass [OK] 2022-09-06T18:24:00,771 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #10: TransitionFinderPass 2022-09-06T18:24:00,836 [main] INFO a.f.a.t.a.p.TransitionPassImpl - > Found 1 initializing transitions 2022-09-06T18:24:00,845 [main] INFO a.f.a.t.a.p.TransitionPassImpl - > Found 1 transitions 2022-09-06T18:24:00,846 [main] INFO a.f.a.t.a.p.TransitionPassImpl - > No constant initializer 2022-09-06T18:24:00,847 [main] INFO a.f.a.t.a.p.TransitionPassImpl - > Applying unique renaming 2022-09-06T18:24:00,869 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #10: TransitionFinderPass [OK] 2022-09-06T18:24:00,870 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #11: OptimizationPass 2022-09-06T18:24:00,874 [main] INFO a.f.a.t.p.p.OptPassImpl - > Applying optimizations: 2022-09-06T18:24:00,875 [main] INFO a.f.a.t.p.p.OptPassImpl - > ConstSimplifier 2022-09-06T18:24:00,879 [main] INFO a.f.a.t.p.p.OptPassImpl - > ExprOptimizer 2022-09-06T18:24:00,885 [main] INFO a.f.a.t.p.p.OptPassImpl - > SetMembershipSimplifier 2022-09-06T18:24:00,887 [main] INFO a.f.a.t.p.p.OptPassImpl - > ConstSimplifier 2022-09-06T18:24:00,888 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #11: OptimizationPass [OK] 2022-09-06T18:24:00,889 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #12: AnalysisPass 2022-09-06T18:24:00,891 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Marking skolemizable existentials and sets to be expanded... 2022-09-06T18:24:00,892 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Skolemization 2022-09-06T18:24:00,893 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Expansion 2022-09-06T18:24:00,896 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Remove unused let-in defs 2022-09-06T18:24:00,898 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Running analyzers... 2022-09-06T18:24:00,909 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Introduced expression grades 2022-09-06T18:24:00,912 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #12: AnalysisPass [OK] 2022-09-06T18:24:00,914 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #13: BoundedChecker 2022-09-06T18:24:02,581 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0 2022-09-06T18:24:02,582 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT... 2022-09-06T18:24:02,741 [main] ERROR a.f.a.t.Tool\$ - test.tla:15:62-15:77: rewriter error: Range bounds are too large to fit in scala.Int at.forsyte.apalache.infra.AdaptedException: test.tla:15:62-15:77: rewriter error: Range bounds are too large to fit in scala.Int at at.forsyte.apalache.infra.Executor.run(Executor.scala:37) at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:87) at at.forsyte.apalache.tla.Tool\$.runCommand(Tool.scala:135) at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:115) at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:36) at at.forsyte.apalache.tla.Tool.main(Tool.scala) ```

System information

Triage checklist (for maintainers)

konnov commented 2 years ago

There is an issue with the error message. It should have told you that your set is a bit too large to deal with.

Here is what it gets preprocessed into:

Init_si_0000 ==
  Skolem((\E t_a$1 \in SUBSET ({
    [denom |-> d$1, amount |-> a$1]:
      d$1 \in { "a", "b", "c" },
      a$1 \in
        0
          .. 115792089237316195423570985008687907853269984665640564039457584007913129639935
  }):
    Skolem((\E t_9$1 \in { "Alice", "Bob", "Carol", "Dave", "Eve" }:
      Skolem((\E t_8$1 \in { "Alice", "Bob", "Carol", "Dave", "Eve" }:
        action' := [sender |-> t_8$1, receiver |-> t_9$1, coins |-> t_a$1]))))))

So the error message is not very informative, but there is no way we can construct a powerset of the set 0.. 115792089237316195423570985008687907853269984665640564039457584007913129639935.

If you avoid sets of records, especially the ones with immensely large powersets, then you have better chances.

konnov commented 2 years ago

Classifying it as usability issue, as this is concerned with a suboptimal error message.

shonfeder commented 2 years ago

re: simplifying selection of action, perhaps something like this?

---- MODULE Ex ----
EXTENDS Apalache, Integers

VARIABLES
    \* @typeAlias: COIN = {denom: Str, amount: Int};
    \* @typeAlias: ACTION = {sender: Str, receiver: Str, coins: Set(COIN)};
    \* @type: ACTION;
    action

WALLETS == {"Alice", "Bob", "Carol", "Dave", "Eve"}
MAX_BALANCE == 10

DENOMS == {"a", "b", "c"}

COINS == { [denom |-> d, amount |-> a] : d \in DENOMS, a \in 0 .. MAX_BALANCE }

Actions == [ sender: WALLETS, receiver: WALLETS, coins: SUBSET COINS ]

Init == action \in Actions

Next == \E a \in Actions: action' = a
=====
konnov commented 2 years ago

Right, this works. However, the problem was not with big integers, which we support, but with a..b over big integers in combination with SUBSET, which in this case forces us to reason about sets of size up to $2^{256}$. This would require a quantified encoding.

shonfeder commented 2 years ago

Right, sorry, that was orthoginal to the big ints thing. I was only addressing

Besides that, what I want to achieve, is to express a non-deterministic choice of action. It should be possible to do simpler than in the example; I would be grateful for help on how to express the desired behavior by possibly other means.

Maybe I misunderstood what was being asked, and maybe my suggestion is not really a simplification (it amounts to the same any how). But I took that to be unrelated to the big int issue. I just changed MAX_BALANCE so the spec would run :)

andrey-kuprianov commented 2 years ago

As has been hinted by @konnov, Value Generators seem to be a better approach here than constructing power sets.

andrey-kuprianov commented 2 years ago

Related to #2139 (cc @danwt, @konnov ); this is what I ended up using to get nice variability wrt. generated actions:

---- MODULE test ----
EXTENDS Apalache, Integers

VARIABLES
    \* @typeAlias: COIN = [denom: Str, amount: Int];
    \* @typeAlias: ACTION = [sender: Str, receiver: Str, coins: Int -> COIN];
    \* @type: ACTION;
    action,
    \* @type: Int;
    step

MAX_BALANCE == 2^256-1

WALLETS == {"Alice", "Bob", "Carol", "Dave", "Eve"}
DENOMS == {"a", "b", "c"}
AMOUNTS == { 0, 1, 2, 3, 10, 20, 30, 100, 200, 300, 2^256-2, 2^256-1, 2^256, 2^256+1, 2^256+2 }

COINS == [ denom : DENOMS, amount: AMOUNTS ]

\* @type: COIN;
GuessCoin ==
  LET d == Guess(DENOMS) IN 
  LET a == Guess(AMOUNTS) IN 
    [ denom |-> d, amount |-> a ]

\* @type: Int -> COIN;
GuessCoins == [ n \in 1..2 |-> GuessCoin ]

\* @type: (ACTION) => Bool;
NewAction(a) ==
  \E sender, receiver \in WALLETS:
    a = [ sender |-> sender, receiver |-> receiver, coins |-> GuessCoins ]

Init == NewAction(action) /\ step=0

Next == NewAction(action') /\ step'=step+1

View == action

Inv == step<4
=====

and, e.g. apalache check --inv=Inv --max-error=20 --view=View test.tla

Would be interested to hear opinions on whether this is a good approach or not, and if it can be improved.

konnov commented 2 years ago

Looks like a nice PBT test. You do not need the invariant in this case, you could just run:

apalache-mc simulate --length=4 --max-error=20 --view=View test.tla

You could also write Guess(AMOUNTS \union {Gen(1)}) to add a bit of variability.