[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Rivers Xiao <riversshallberevealed@xxxxxxxxx>*Date*: Fri, 14 Apr 2023 08:45:09 -0700 (PDT)

Hi, guys, I am currently running simulation on my spec. I get this error before the simulation even starts

Error: Attempted to apply the operator overridden by the Java method

public static tlc2.value.impl.Value tlc2.module.TLC.Permutations(tlc2.value.impl.Value),

but it produced the following error:

-2102132736

Then I changed my init state so it would lead to shorter trace and get

Error: TLC threw an unexpected exception.

This was probably caused by an error in the spec or model.

See the User Output or TLC Console for clues to what happened.

The exception was a util.WrongInvocationException

: Attempted to construct a set with too many elements (>1000000).

Then I explicitly set maxSetSize to 2147483647. But I need to wait like an hour before the simulator reports "Computed 1 initial states..." and starts the simulation.

It seems before the simulation starts, simulator does some computations which invoke Permutations to compute sets. But I only has one possible init state and it was set by constants. Why does it take so long for simulator to run before simulation starts (even throws an error) when init state is already set?

-- You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e8f2f6b4-efc3-4a79-979b-ef450399112bn%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Computations before simulation starts***From:*Markus Kuppe

- Prev by Date:
**[tlaplus] Re: Analysis: Runway, a new formal specification system** - Next by Date:
**Re: [tlaplus] Computations before simulation starts** - Previous by thread:
**Re: [tlaplus] TLA+ project meeting video or minutes** - Next by thread:
**Re: [tlaplus] Computations before simulation starts** - Index(es):